Proof of Nichomacus's theorem in Coq.

gistfile1.v

(* Ported from Dan Peebles's proof at: https://gist.github.com/2356060 *)
Module SquaredTriangular.
Require Import Arith.

Definition N := nat.

(* Sigma notation for expressing sums. *)
Fixpoint Σ (x : N) (f : N -> N) : N :=
  match x with
  | 0 => 0
  | S x' => Σ x' f + f x
  end.

(* Notation of dubious utility. *)
Notation "X ²" := (X * X) (at level 10).

Lemma id_simpl : forall T (X:T), id X = X. auto. Qed.

Lemma sum_nats : forall n, 2 * Σ n (@id N) = (1 + n) * n.
Proof. 
  induction n; auto. simpl. rewrite id_simpl.

  (* algebra *) 
  match goal with
  | |- ?L = _ => replace L with (2 * Σ n id + S n + S n) by ring
  end.

  (* induction *)
  rewrite IHn. ring.
Qed.

Lemma square_expand : forall X Y, (X + Y) ² = X * X + 2 * X * Y + Y * Y.
Proof. intros. ring. Qed.

Definition cube X := X * X ².

Theorem Nichomacus : forall n, Σ n id ² = Σ n cube.
Proof.
  induction n; auto. simpl. rewrite id_simpl.
  rewrite square_expand. rewrite sum_nats.
  rewrite IHn. unfold cube at 3. ring. 
Qed.