∀ n m, n < m ⇒ (div n m) = O

Theorem eq_div_O : forall (n:nat.nat), forall (m:nat.nat), (nat.lt n m) -> logic.eq (nat.nat) (div n m) nat.O.

theorem eq_div_O : \forall (n:nat). \forall (m:nat). ((lt) n m) -> (eq) (nat) ((div) n m) (O) .

theorem eq_div_O : forall (n:nat.nat) , forall (m:nat.nat) , ((((nat.lt_) ) (n)) (m)) -> (((logic.eq_) (nat.nat)) ((((div_mod.div) ) (n)) (m))) ((nat.O) ).

eq_div_O : LEMMA (FORALL(n:nat_sttfa_th.sttfa_nat):(FORALL(m:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.lt(n)(m) => logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](div_mod_sttfa.div(n)(m))(nat_sttfa_th.sttfa_O))))

Printing for OpenTheory is not working at the moment.