∀ p n m, n ≤ p ⇒ (mod_aux p n m) ≤ m

Theorem le_mod_aux_m_m : forall (p:nat.nat), forall (n:nat.nat), forall (m:nat.nat), (nat.le n p) -> nat.le (mod_aux p n m) m.

theorem le_mod_aux_m_m : \forall (p:nat). \forall (n:nat). \forall (m:nat). ((le) n p) -> (le) ((mod_aux) p n m) m.

theorem le_mod_aux_m_m : forall (p:nat.nat) , forall (n:nat.nat) , forall (m:nat.nat) , ((((nat.le_) ) (n)) (p)) -> (((nat.le_) ) (((((div_mod.mod_aux) ) (p)) (n)) (m))) (m).

le_mod_aux_m_m : LEMMA (FORALL(p:nat_sttfa_th.sttfa_nat):(FORALL(n:nat_sttfa_th.sttfa_nat):(FORALL(m:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.le(n)(p) => nat_sttfa_th.le(div_mod_sttfa.mod_aux(p)(n)(m))(m)))))

Printing for OpenTheory is not working at the moment.