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