∀ p n m, n = (((div_aux p n m) × (m+1)) + (mod_aux p n m))

Theorem div_aux_mod_aux : forall (p:nat.nat), forall (n:nat.nat), forall (m:nat.nat), logic.eq (nat.nat) n (nat.plus (nat.times (div_aux p n m) (nat.S m)) (mod_aux p n m)).

theorem div_aux_mod_aux : \forall (p:nat). \forall (n:nat). \forall (m:nat). (eq) (nat) n ((plus) ((times) ((div_aux) p n m) ((S) m)) ((mod_aux) p n m)).

theorem div_aux_mod_aux : forall (p:nat.nat) , forall (n:nat.nat) , forall (m:nat.nat) , (((logic.eq_) (nat.nat)) (n)) ((((nat.plus) ) ((((nat.times) ) (((((div_mod.div_aux) ) (p)) (n)) (m))) (((nat.S) ) (m)))) (((((div_mod.mod_aux) ) (p)) (n)) (m))).

div_aux_mod_aux : LEMMA (FORALL(p:nat_sttfa_th.sttfa_nat):(FORALL(n:nat_sttfa_th.sttfa_nat):(FORALL(m:nat_sttfa_th.sttfa_nat):logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](n)(nat_sttfa_th.plus(nat_sttfa_th.times(div_mod_sttfa.div_aux(p)(n)(m))(nat_sttfa_th.sttfa_S(m)))(div_mod_sttfa.mod_aux(p)(n)(m))))))

Printing for OpenTheory is not working at the moment.