(a + b)^2 = a^2 + 2 * a * b + b ^2 proof

Lemma sameFunc : forall a b : nat, forall f : (nat->nat), a = b -> (f a) = (f b).
Proof.
  intros.
  subst.
  trivial.
Qed.


Lemma eqOrder : forall a b : nat, a = b -> b = a.
Proof.
  intros.
  subst.
  reflexivity.
Qed.

Lemma eqStep : forall n : nat, (n + 1) = (S n).
Proof.
  intros.
  elim n.
  simpl.
  reflexivity.
  intros.
  simpl.
  remember (n0 + 1) as a.
  remember (S n0) as b.
  apply sameFunc.
  apply H.
Qed.

Lemma nextGreaterS : forall n : nat, (S n) > n.
Proof.
  unfold gt.
  unfold lt.
  intros.
  remember (S n) as k.
  apply le_n.
Qed.

Lemma nextGreaterPlus: forall n : nat, (n + 1) > n.
Proof.
  intros.
  replace (n + 1) with (S n).
  apply nextGreaterS.
  remember (S n) as a.
  remember (n + 1) as b.
  apply eqOrder.
  replace a with (S n).
  replace b with (n + 1).
  apply eqStep.
Qed.

Lemma addZeroAfter : forall a : nat, a + 0 = a.
Proof.
  intros.
  elim a.
  Focus 1.
  simpl.
  reflexivity.
  simpl.
  intros.
  remember (n + 0) as k.
  replace k with n.
  apply sameFunc.
  reflexivity.
Qed.

Lemma addZeroBefore : forall a : nat, 0 + a = a.
Proof.
  intros.
  unfold Nat.add.
  reflexivity.
Qed.

Lemma addOneToAnother : forall a b : nat, (S a) + b = a + (S b).
Proof.
  intros.
  elim a.
  remember (S b) as k.
  Focus 1.
  replace (0 + k) with (k + 0).
  Focus 2.
  replace (k + 0) with k.
  Focus 2.
  apply eqOrder.
  apply addZeroAfter.
  apply addZeroBefore.
  replace (k + 0) with k.
  Focus 2.
  apply eqOrder.
  apply addZeroAfter.
  replace k with (S b).
  replace (1 + b) with (b + 1).
  Focus 2.
  simpl.
  apply eqStep.
  remember b as n.
  apply eqStep.
  simpl.
  intros.
  apply sameFunc.
  apply H.
Qed.

Lemma addComm : forall a b : nat, a + b = b + a.
Proof.
  intros.
  elim a.
  simpl.
  Focus 1.
  apply eqOrder.
  apply addZeroAfter.
  intros.
  replace (b + (S n)) with ((S b) + n).
  Focus 2.
  apply addOneToAnother.
  simpl.
  apply sameFunc.
  apply H.
Qed.

Lemma mulNext : forall m n, (m + 1) * n = m * n + n.
Proof.
  intros.
  replace (m + 1) with (S m).
  Focus 2.
  apply eqOrder.
  apply eqStep.
  unfold Nat.mul.
  simpl.
  fold Nat.mul.
  remember (m * n) as a.
  apply addComm.
Qed.

Lemma mulByZero : forall n, n * 0 = 0.
Proof.
  intros.
  elim n.
  simpl.
  reflexivity.
  intros.
  replace (S n0) with (n0 + 1).
  Focus 2.
  apply eqStep.
  replace ((n0 + 1) * 0) with (n0 * 0 + 0).
  Focus 2.
  apply eqOrder.
  apply mulNext.
  replace (n0 * 0) with 0.
  simpl.
  reflexivity.
Qed.


Lemma mulByOne : forall n, n * 1 = n.
Proof.
  intros.
  elim n.
  simpl.
  reflexivity.
  intros.
  replace (n0 * 1) with n0.
  simpl.
  apply sameFunc.
  apply H.
Qed.

Lemma addNotDependsOnOrder: forall a b c, (a + b) + c = a + (b + c).
Proof.
  intros.
  elim a.
  simpl.
  reflexivity.
  simpl.
  intros.
  apply sameFunc.
  apply H.
Qed.

Lemma mulAssoc: forall a b c, (a + b) * c = a * c + b * c.
Proof.
  intros.
  elim a.
  simpl.
  reflexivity.
  simpl.
  intros.
  remember ((n + b) * c) as A.
  remember (n * c) as t1.
  remember (b * c) as t2.
  replace A with (t1 + t2).
  apply eqOrder.
  apply addNotDependsOnOrder.
Qed.

Lemma mulByZeroFromDifferentSide : forall a : nat, 0 * a = 0.
Proof.
  intros.
  simpl.
  reflexivity.
Qed.

Require Import ZArith.

Lemma mulNextFromDifferentSide : forall a b, a * (b + 1) = a * b + a.
Proof.
  intros.
  elim a.
  replace (0 * (b + 1)) with 0.
  replace (0 * b) with 0.
  simpl.
  reflexivity.
  apply eqOrder.
  apply mulByZeroFromDifferentSide.
  apply eqOrder.
  apply mulByZeroFromDifferentSide.
  intros.
  replace (S n) with (n + 1).
  replace ((n + 1) * (b + 1)) with ((n * (b + 1)) + (b + 1)).
  Focus 1.
  replace (n * (b + 1)) with (n * b + n).
  remember (n * b + n) as A.
  replace (A + (b + 1)) with (A + b + 1).
  replace ((n + 1) * b) with (n * b + b).
  replace A with (n * b + n).
  remember (n * b + b) as B.
  replace (B + (n + 1)) with (B + n + 1).
  replace B with (n * b + b).
  replace (n * b + n + b) with (n * b + b + n).
  reflexivity.
  remember (n * b) as C.
  replace (C + b + n) with (C + (b + n)).
  replace (b + n) with (n + b).
  replace (C + (n + b)) with (C + n + b).
  reflexivity.
  apply addNotDependsOnOrder.
  apply addComm.
  apply eqOrder.
  apply addNotDependsOnOrder.
  apply addNotDependsOnOrder.
  apply eqOrder.
  apply mulNext.
  apply addNotDependsOnOrder.
  apply eqOrder.
  apply mulNext.
  apply eqStep.
Qed.

Lemma mulComm : forall a b, a * b = b * a.
Proof.
  intros.
  elim a.
  replace (0 * b) with 0.
  replace (b * 0) with 0.
  reflexivity.
  apply eqOrder.
  apply mulByZero.
  apply eqOrder.
  apply mulByZeroFromDifferentSide.
  intros.
  replace (S n) with (n + 1).
  replace ((n + 1) * b) with (n * b + b).
  replace (b * (n + 1)) with (b * n + b).
  replace (n * b) with (b * n).
  reflexivity.
  apply eqOrder.
  apply mulNextFromDifferentSide.
  apply eqOrder.
  apply mulNext.
  apply eqStep.
Qed.


Lemma mulNotDependsOnOrder : forall a b c : nat, a * b * c = a * (b * c).
Proof.
  intros.
  elim c.
  replace (b * 0) with 0.
  replace (a * 0) with 0.
  replace ((a * b) * 0) with 0.
  reflexivity.
  apply eqOrder.
  apply mulByZero.
  apply eqOrder.
  apply mulByZero.
  apply eqOrder.
  apply mulByZero.
  intros.
  replace (S n) with (n + 1).
  replace (b * (n + 1)) with (b * n + b).
  replace (a * (b * n + b)) with ((b * n + b) * a).
  replace (a * b * (n + 1)) with (a * b * n + a * b * 1).
  replace ((b * n + b) * a) with (b * n * a + b * a).
  replace (a * b * 1) with (a * b).
  replace (b * n * a) with (a * b * n).
  replace (a * b) with (b * a).
  reflexivity.
  apply mulComm.
  replace (a * b * n) with (a * (b * n)).
  apply mulComm.
  apply eqOrder.
  apply mulByOne.
  apply eqOrder.
  apply mulAssoc.
  apply eqOrder.
  replace (a * b * n) with (n * (a * b)).
  replace (a * b * 1) with (1 * (a * b)).
  replace (a * b * (n + 1)) with ((n + 1) * (a * b)).
  apply mulAssoc.
  apply mulComm.
  apply mulComm.
  apply mulComm.
  apply mulComm.
  replace (b * n) with (n * b).
  replace (b * (n + 1)) with ((n + 1) * b).
  apply eqOrder.
  apply mulNext.
  apply mulComm.
  apply mulComm.
  apply eqStep.
Qed.


Lemma squareRule : forall a b : nat, (a + b) * (a + b) = a * a + 2 * a * b + b * b.
Proof.
  intros.
  replace ((a + b) * (a + b)) with (a * (a + b) + b * (a + b)).
  Focus 2.
  apply eqOrder.
  apply mulAssoc.
  replace (a * (a + b)) with ((a + b) * a).
  replace (b * (a + b)) with ((a + b) * b).
  replace ((a + b) * a) with (a * a + b * a).
  remember (a * a + b * a) as Q.
  replace ((a + b) * b) with (a * b + b * b).
  replace (Q + (a * b + b * b)) with (Q + a * b + b * b).
  replace Q with (a * a + b * a).
  replace (a * b) with (b * a).
  replace ((a * a) + (b * a) + (b * a)) with (a * a + 2 * a * b).
  reflexivity.
  replace ((a * a) + (b * a) + (b * a)) with (a * a + ((b * a) + (b * a))).
  replace (2 * a * b) with (b * a + b * a).
  reflexivity.
  replace (b * a) with (a * b).
  replace (2 * a * b) with ((1 + 1) * a * b).
  replace ((1 + 1) * a * b) with (1 * a * b + 1 * a * b).
  replace (1 * a * b) with (a * b * 1).
  replace (a * b * 1) with (a * b).
  reflexivity.
  apply eqOrder.
  apply mulByOne.
  replace (a * b * 1) with (a * b).
  replace (1 * a) with (a * 1).
  replace (a * 1) with a.
  reflexivity.
  apply eqOrder.
  apply mulByOne.
  apply mulComm.
  apply eqOrder.
  apply mulByOne.
  apply eqOrder.
  replace (1 * a * b) with (1 * (a * b)).
  replace ((1 + 1) * a * b) with ((1 + 1) * (a * b)).
  apply mulAssoc.
  apply eqOrder.
  apply mulNotDependsOnOrder.
  apply eqOrder.
  apply mulNotDependsOnOrder.
  replace (1 + 1) with 2.
  reflexivity.
  simpl.
  reflexivity.
  apply mulComm.
  apply eqOrder.
  apply addNotDependsOnOrder.
  apply mulComm.
  apply addNotDependsOnOrder.
  apply eqOrder.
  apply mulAssoc.
  apply eqOrder.
  apply mulAssoc.
  apply eqOrder.
  apply mulComm.
  apply mulComm.
Qed.