proposition: Theorem mul_succ_r : forall n m, n * (S m) == n * m + n.
proof: Proof. intros n m; nzinduct n. - now nzsimpl. - intro n. nzsimpl. rewrite succ_inj_wd, <- add_assoc, (add_comm m n), add_assoc. now rewrite add_cancel_r. Qed.
imports: NZAxioms NZBase NZAdd