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

Theorem

div_mod.eq_times_div_minus_mod

Statement

∀ a b, ((div a b) × b) = (a - (mod a b))

Main Dependencies
Theory

Coq-Jumb
Statement

Theorem eq_times_div_minus_mod : forall (a:nat.nat), forall (b:nat.nat), logic.eq (nat.nat) (nat.times (div a b) b) (nat.minus a (mod a b)).



Matita-Jumb
Statement

theorem eq_times_div_minus_mod : \forall (a:nat). \forall (b:nat). (eq) (nat) ((times) ((div) a b) b) ((minus) a ((mod) a b)).



Lean-jumb
Statement

theorem eq_times_div_minus_mod : forall (a:nat.nat) , forall (b:nat.nat) , (((logic.eq_) (nat.nat)) ((((nat.times) ) ((((div_mod.div) ) (a)) (b))) (b))) ((((nat.minus) ) (a)) ((((div_mod.mod) ) (a)) (b))).



PVS-jumb

Statement

eq_times_div_minus_mod : LEMMA (FORALL(a:nat_sttfa_th.sttfa_nat):(FORALL(b:nat_sttfa_th.sttfa_nat):logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](nat_sttfa_th.times(div_mod_sttfa.div(a)(b))(b))(nat_sttfa_th.minus(a)(div_mod_sttfa.mod(a)(b)))))



OpenTheory

Printing for OpenTheory is not working at the moment.