∀ n m q r, r < m ⇒ n = ((q × m) + r) ⇒ div_mod_spec n m q r

Axiom div_mod_spec_intro : forall (n:nat.nat), forall (m:nat.nat), forall (q:nat.nat), forall (r:nat.nat), (nat.lt r m) -> (logic.eq (nat.nat) n (nat.plus (nat.times q m) r)) -> div_mod_spec n m q r

axiom div_mod_spec_intro : \forall (n:nat). \forall (m:nat). \forall (q:nat). \forall (r:nat). ((lt) r m) -> ((eq) (nat) n ((plus) ((times) q m) r)) -> (div_mod_spec) n m q r

axiom div_mod_spec_intro : forall (n:nat.nat) , forall (m:nat.nat) , forall (q:nat.nat) , forall (r:nat.nat) , ((((nat.lt_) ) (r)) (m)) -> ((((logic.eq_) (nat.nat)) (n)) ((((nat.plus) ) ((((nat.times) ) (q)) (m))) (r))) -> (((((div_mod.div_mod_spec) ) (n)) (m)) (q)) (r)

div_mod_spec_intro : AXIOM (FORALL(n:nat_sttfa_th.sttfa_nat):(FORALL(m:nat_sttfa_th.sttfa_nat):(FORALL(q:nat_sttfa_th.sttfa_nat):(FORALL(r:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.lt(r)(m) => (logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](n)(nat_sttfa_th.plus(nat_sttfa_th.times(q)(m))(r)) => div_mod_sttfa.div_mod_spec(n)(m)(q)(r)))))))

Printing for OpenTheory is not working at the moment.