proposition: Theorem mul_assoc : forall n m p, n * (m * p) == (n * m) * p.
proof: Proof. intros n m p; nzinduct n. - now nzsimpl. - intro n. nzsimpl. rewrite mul_add_distr_r. now rewrite add_cancel_r. Qed.
imports: NZAxioms NZBase NZAdd