// This prints the left floatting menu
Dedukti    Load Matita      Load Coq         Load Lean        Load PVS         Load OpenTheory Load
Dedukti-jumb

Theorem

div_mod.le_mod_aux_m_m

Statement

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

Main Dependencies
Theory

Coq-Jumb
Statement

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.



Matita-Jumb
Statement

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.



Lean-jumb
Statement

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).



PVS-jumb

Statement

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)))))



OpenTheory

Printing for OpenTheory is not working at the moment.