∀ a b, O < b ⇒ (div (a × b) b) = a

Theorem div_times : forall (a:nat.nat), forall (b:nat.nat), (nat.lt nat.O b) -> logic.eq (nat.nat) (div (nat.times a b) b) a.

theorem div_times : \forall (a:nat). \forall (b:nat). ((lt) (O) b) -> (eq) (nat) ((div) ((times) a b) b) a.

theorem div_times : forall (a:nat.nat) , forall (b:nat.nat) , ((((nat.lt_) ) ((nat.O) )) (b)) -> (((logic.eq_) (nat.nat)) ((((div_mod.div) ) ((((nat.times) ) (a)) (b))) (b))) (a).

div_times : LEMMA (FORALL(a:nat_sttfa_th.sttfa_nat):(FORALL(b:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.lt(nat_sttfa_th.sttfa_O)(b) => logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](div_mod_sttfa.div(nat_sttfa_th.times(a)(b))(b))(a))))

Printing for OpenTheory is not working at the moment.