proposition: Theorem mul_succ_l : forall n m, (Z.succ n) * m == n * m + m.
proof: Proof. intros (n1,n2) (m1,m2); unfold Z.mul, Z.succ, Z.eq; simpl; nzsimpl. rewrite <- (add_assoc _ m1), (add_comm m1), (add_assoc _ _ m1). now rewrite <- (add_assoc _ m2), (add_comm m2), (add_assoc _ (n2*m1)%N m2). Qed.
imports: NSub ZAxioms Ring