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

Theorem

div_mod.div_mod

Statement

∀ n m, n = (((div n m) × m) + (mod n m))

Main Dependencies
Theory

Coq-Jumb
Statement

Theorem div_mod : forall (n:nat.nat), forall (m:nat.nat), logic.eq (nat.nat) n (nat.plus (nat.times (div n m) m) (mod n m)).



Matita-Jumb
Statement

theorem div_mod : \forall (n:nat). \forall (m:nat). (eq) (nat) n ((plus) ((times) ((div) n m) m) ((mod) n m)).



Lean-jumb
Statement

theorem div_mod : forall (n:nat.nat) , forall (m:nat.nat) , (((logic.eq_) (nat.nat)) (n)) ((((nat.plus) ) ((((nat.times) ) ((((div_mod.div) ) (n)) (m))) (m))) ((((div_mod.mod) ) (n)) (m))).



PVS-jumb

Statement

div_mod : LEMMA (FORALL(n:nat_sttfa_th.sttfa_nat):(FORALL(m:nat_sttfa_th.sttfa_nat):logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](n)(nat_sttfa_th.plus(nat_sttfa_th.times(div_mod_sttfa.div(n)(m))(m))(div_mod_sttfa.mod(n)(m)))))



OpenTheory

Printing for OpenTheory is not working at the moment.