∀ n m, O < m ⇒ div_mod_spec n m (div n m) (mod n m)

Theorem div_mod_spec_div_mod : forall (n:nat.nat), forall (m:nat.nat), (nat.lt nat.O m) -> div_mod_spec n m (div n m) (mod n m).

theorem div_mod_spec_div_mod : \forall (n:nat). \forall (m:nat). ((lt) (O) m) -> (div_mod_spec) n m ((div) n m) ((mod) n m).

theorem div_mod_spec_div_mod : forall (n:nat.nat) , forall (m:nat.nat) , ((((nat.lt_) ) ((nat.O) )) (m)) -> (((((div_mod.div_mod_spec) ) (n)) (m)) ((((div_mod.div) ) (n)) (m))) ((((div_mod.mod) ) (n)) (m)).

div_mod_spec_div_mod : LEMMA (FORALL(n:nat_sttfa_th.sttfa_nat):(FORALL(m:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.lt(nat_sttfa_th.sttfa_O)(m) => div_mod_sttfa.div_mod_spec(n)(m)(div_mod_sttfa.div(n)(m))(div_mod_sttfa.mod(n)(m)))))

Printing for OpenTheory is not working at the moment.