proposition: Theorem mul_add_distr_l : forall n m p, n * (m + p) == n * m + n * p.
proof: Proof. intros n m p. rewrite (mul_comm n (m + p)), (mul_comm n m), (mul_comm n p). apply mul_add_distr_r. Qed.
imports: NZAxioms NZBase NZAdd