(* Exercise coq_nat_09 *)

(* Now, let us prove that multiplication is commutative *)

(* For this we may need to use some properties of addition and multiplication  
   that we proved before. *)
Require Import Arith.
Check mult_0_r.
Check plus_comm.
Check plus_assoc.

(* ... and a following auxiliary lemma *)

Lemma mult_succ : forall m n, n + n * m = n * S m.
Proof.
intros.
(* Rule of thumb: Do induction over the argument that 
   the function does recursion over.
   For plus and mult, that is the first argument *)
induction n.
- simpl.
 reflexivity.
(* General pattern that often works:
   = simpl (to do some computation steps with teh defined functions)
   = find a way to rewrite with the IH 
   = use auxiliary lemmas *)
- simpl.
  rewrite <- IHn.
  rewrite plus_assoc.
  rewrite (plus_comm n m).
  (* Note the explicit argument I give to plus_comm 
     to rewrite the specific subterm *)
  rewrite <- plus_assoc.
  reflexivity.
Qed.

Lemma mult_comm : forall m n, m * n = n * m.

Proof.
intros.
induction n.
- simpl.
  rewrite mult_0_r.
  reflexivity.
- simpl.
  rewrite <- IHn.
  rewrite mult_succ.
  reflexivity.
Qed.

(* As commutativity is very much a symmetric property in the two
   arguments, you can also do induction m and the proof is basically 
   the same *)
Lemma mult_comm' : forall m n, m * n = n * m.

Proof.
intros.
induction m.
- simpl.
  rewrite mult_0_r.
  reflexivity.
- simpl.
  rewrite IHm.
  rewrite mult_succ.
  reflexivity.
Qed.