Proof of the commutativity and associativity of (N, +) (N, ×)

plus_comm.v

Require Import Arith.

Theorem plus_assoc_r: forall l n m : nat, l + (m + n) = (l + m) + n.
Proof.
  intros.
  induction l.
  rewrite plus_0_l.
  rewrite plus_0_l with (n := m).
  reflexivity.
  rewrite plus_Sn_m.
  rewrite plus_Sn_m with (n := l) (m := m).
  rewrite plus_Sn_m with (n := l + m) (m := n).
  f_equal.
  exact IHl.
Qed.

Lemma plus_S_1_l: forall n : nat, S n = 1 + n.
  intros.
  rewrite plus_Sn_m, plus_0_l.
  reflexivity.
Qed.  

Lemma plus_S_1_r: forall n : nat, S n = n + 1.
  induction n.
  rewrite plus_0_l.
  reflexivity.
  rewrite plus_Sn_m.
  f_equal.
  exact IHn.
Qed.

Theorem my_plus_comm: forall n m : nat, n + m = m + n.
Proof.
  intros.
  induction n.
  induction m.
  reflexivity.
  rewrite plus_0_r, plus_0_l.
  reflexivity.
  rewrite plus_Sn_m.
  rewrite plus_S_1_l with (n := n).
  rewrite plus_assoc_r, <-plus_S_1_r, plus_Sn_m.
  f_equal.
  exact IHn.
Qed.

Lemma mult_1_r: forall n: nat, n * 1 = n.
Proof.
  intros.
  induction n.
  rewrite mult_0_l.
  reflexivity.
  rewrite mult_succ_l.
  rewrite IHn.
  rewrite <-plus_S_1_r .
  reflexivity.
Qed.

Theorem mult_plus_distr_r: forall n m l : nat, n * m + n * l = n * (m + l).
Proof.
  intros.
  induction n.
  rewrite mult_0_l, mult_0_l, mult_0_l, plus_0_l.
  reflexivity.
  rewrite mult_succ_l, mult_succ_l, mult_succ_l.
  rewrite plus_assoc_r.
  rewrite <-((plus_assoc_r) (n*m) (n*l) m).
  rewrite (my_plus_comm m (n*l)).
  rewrite plus_assoc_r.
  rewrite IHn.
  rewrite plus_assoc_r.
  reflexivity.
Qed.

Theorem my_mult_comm : forall n m : nat, n * m = m * n.
Proof.
  intros.
  induction n.
  rewrite mult_0_l.
  induction m.
  rewrite mult_0_l.
  reflexivity.
  rewrite mult_succ_l.
  rewrite <-IHm.
  rewrite plus_0_l.
  reflexivity.
  rewrite mult_succ_l.
  rewrite IHn.
  rewrite my_plus_comm.
  rewrite <-mult_1_r with (n := m) at 1.
  rewrite mult_plus_distr_r.
  rewrite <-plus_S_1_l.
  reflexivity.
Qed.

Theorem my_plus_0_r: forall n : nat, n * 0 = 0.
Proof.
  intros.
  rewrite mult_comm, mult_0_l.
  reflexivity.
Qed.

Theorem mult_plus_distr_l : forall n m l : nat, n * l + m * l = (n + m) * l.
  intros.
  rewrite (mult_comm n l), (mult_comm m l), mult_plus_distr_r.
  rewrite mult_comm at 1.
  reflexivity.
Qed.

Theorem mult_1_l : forall n : nat, 1 * n = n.
Proof.
  intros.
  rewrite mult_comm.
  rewrite mult_1_r.
  reflexivity.
Qed.

Theorem mult_assoc_r: forall n m l : nat, n * (m * l) = (n * m) * l.
Proof.
  intros.
  induction n.
  rewrite mult_0_l, mult_0_l.
  reflexivity.
  rewrite mult_succ_l, mult_succ_l.
  rewrite IHn.
  rewrite mult_plus_distr_l.
  reflexivity.
Qed.