m * n = n * m

commutative.v

Lemma mult_0_r : forall n:nat,
  n * 0 = 0.
Proof.
  intros n. induction n as [| n'].
  (* Case "n = 0". *)
    simpl.
    reflexivity.
  (* Case "n = S n'". *)
    simpl.
    rewrite -> IHn'.
    reflexivity.
Qed.

Lemma plus_0_r : forall n:nat, n + 0 = n.
Proof.
  intros n. induction n as [| n'].
  reflexivity.
  simpl.
  rewrite -> IHn'.
  reflexivity.
Qed.

Lemma plus_n_Sm : forall n m : nat, 
  S (n + m) = n + (S m).
Proof. 
  intros n. induction n as [| n'].
  (* Case "n = 0". *)
    simpl.
    reflexivity.
  (* Case "n = S n'". *)
    simpl.
    intros m.
    rewrite -> IHn'.
    reflexivity.
Qed.

Lemma plus_comm : forall n m : nat,
  n + m = m + n.
Proof.
  intros n. induction n as [| n'].
  (* Case "n = 0". *)
    simpl. 
    intros n. 
    rewrite -> plus_0_r.
    reflexivity.
  (* Case "n = S n'". *)
    simpl.
    intros n.
    rewrite -> IHn'.
    rewrite -> plus_n_Sm.
    reflexivity.
Qed.

Lemma abc_bac : forall a b c : nat,
  a + (b + c) = b + (a + c).
Proof.
  induction c as [| c'].
  (* Case "c = 0" *)
    rewrite plus_0_r.
    rewrite plus_0_r.
    rewrite plus_comm.
    reflexivity.
  (* Case "c = S c'" *)
    simpl.
    rewrite <- plus_n_Sm.
    rewrite <- plus_n_Sm.
    rewrite <- plus_n_Sm.
    rewrite <- plus_n_Sm.
    rewrite IHc'.
    reflexivity.
Qed.

Theorem mult_commutativity : forall n m : nat,
  n * m = m * n.
Proof.
  intros n.
  induction n as [| n'].
  (* Case "n = 0". *)
    simpl.
    intros m.
    rewrite mult_0_r.
    reflexivity.
  (* Case "n = S n'". *)
    intros m.
    induction m as [| m'].
    (* Case "m = 0". *)
      simpl.
      rewrite -> mult_0_r.
      reflexivity.
    (* Case "m = S m'". *)
      simpl.
      rewrite -> IHn'.
      simpl.
      f_equal.
      rewrite <- IHm'.
      simpl.
      rewrite -> IHn'.
      rewrite abc_bac.
      reflexivity.
Qed.