Proofs on addition and multiplication in Coq

begin.v

Fixpoint add (x:nat) (y:nat) : nat :=
  match x with
    | 0 => y
    | S z => S (add z y)
  end.

Lemma add_0 : forall x, add x 0 = x.
  intros x.
  induction x.
  - reflexivity.
  - simpl.
    rewrite IHx.
    reflexivity.
Qed.

Lemma add_S : forall x y, add x (S y) = S (add x y).
  intros x.
  induction x; intros y.
  - reflexivity.
  - simpl.
    rewrite IHx.
    reflexivity.
Qed.

Lemma add_sym : forall x y, add x y = add y x.
  intros x.
  induction x; intros y.
  - rewrite add_0.
    reflexivity.
  - simpl.
    rewrite IHx.
    rewrite add_S.
    reflexivity.
Qed.

Lemma add_assoc : forall x y z, add x (add y z) = add (add x y) z.
  intros x y.
  revert x.
  induction y; intros x z.
  - rewrite add_sym with x 0.
    reflexivity.
  - rewrite add_sym.
    simpl.
    rewrite add_sym.
    rewrite IHy.
    rewrite add_sym with x (S y).
    rewrite add_sym with x y.
    reflexivity.
Qed.

Inductive Even : nat -> Prop :=
| even_zero : Even 0
| even_step x y (STEP: x = S (S y)) (IND: Even y) : Even x.

Lemma even_double : forall x, Even (add x x).
  intros x.
  induction x.
  - simpl.
    apply even_zero.
  - simpl.
    rewrite add_sym.
    simpl.
    apply even_step with (add x x).
    + reflexivity.
    + assumption.
Qed.

Fixpoint mult (x:nat) (y:nat) :=
  match x with
    | 0 => 0
    | S z => add (mult z y) y
  end.

Lemma mult_0 : forall x, mult x 0 = 0.
  induction x.
  - simpl.
    reflexivity.
  - simpl.
    rewrite add_sym.
    simpl.
    apply IHx.
Qed.

Lemma mult_S : forall x y, mult y (S x) = add (mult y x) y.
  intros x y.
  induction y.
  - reflexivity.
  - simpl.
    rewrite add_S.
    rewrite add_S.
    rewrite IHy.
    rewrite <- add_assoc.
    rewrite add_sym with y x.
    rewrite add_assoc.
    reflexivity.
Qed.

Lemma mult_sym : forall x y, mult x y = mult y x.
  intros x.
  induction x; intros y.
  - simpl.
    symmetry.
    apply mult_0.
  - rewrite mult_S.
    simpl.
    rewrite IHx.
    reflexivity.
Qed.

Lemma add_mult : forall x y z, mult x (add y z) = add (mult x y) (mult x z).
  intros x y z.
  revert y z.
  induction x; intros y z.
  - reflexivity.
  - simpl.
    rewrite IHx.
    rewrite add_assoc.
    rewrite add_assoc.
    rewrite <- add_assoc with (mult x y) (mult x z) y.
    rewrite add_sym with (mult x z) y.
    rewrite add_assoc.
    reflexivity.
Qed.

Lemma mult_assoc : forall x y z, mult x (mult y z) = mult (mult x y) z.
  intros x y.
  revert x.
  induction y; intros x z.
  - simpl.
    rewrite mult_0.
    reflexivity.
  - simpl.
    rewrite mult_S.
    rewrite add_mult.
    rewrite mult_sym with (add (mult x y) x) z.
    rewrite add_mult.
    rewrite IHy.
    rewrite mult_sym.
    rewrite mult_sym with x z.
    reflexivity.
Qed.

Lemma mult_2_x_even : forall x, Even (mult 2 x).
  intros x.
  induction x.
  - simpl.
    apply even_zero.
  - apply even_step with (mult 2 x).
    + simpl.
      rewrite add_sym.
      simpl.
      reflexivity.
    + assumption.
Qed.