Proof that 5 is prime

prime5.v

Require Arith.
Require Le.

Inductive Divides k : nat -> Prop :=
| Divides_base : Divides k 0
| Divides_step : forall n, Divides k n -> Divides k (k+n).

Definition Prime (p : nat) : Prop :=
  forall k, Divides k p -> (k = 1 \/ k = p).

Theorem divisor_range :
  forall n k, Divides k n -> n = 0 \/ k <= n.
Proof.
  intros n k D;
  induction D; auto with arith.
Qed.

Lemma four_doesnt_divide_five : ~(Divides 4 5).
  intro D.
  inversion D as [| q Q]; subst; simpl.
  pose proof (divisor_range 1 4 Q) as Range.
  destruct Range as [R1 | R2].
  symmetry in R1.
  pose proof (O_S 0); contradiction.
  repeat (apply le_S_n in R2); apply Le.le_n_0_eq in R2.
  pose proof (O_S 2); contradiction.
Qed.

Lemma three_doesnt_divide_five : ~(Divides 3 5).
  intro D.
  inversion D as [| q Q]; subst.
  pose proof (divisor_range 2 3 Q) as Range.
  destruct Range as [R1 | R2].
  symmetry in R1.
  pose proof (O_S 1); contradiction.
  repeat (apply le_S_n in R2); apply Le.le_n_0_eq in R2.
  pose proof (O_S 0); contradiction.
Qed.

Lemma two_doesnt_divide_five : ~(Divides 2 5).
  intro D.
  inversion D as [| q Q]; subst.
  pose proof (divisor_range 3 2 Q) as Range.
  destruct Range as [R1 | R2].
  symmetry in R1.
  pose proof (O_S 2); contradiction.

  inversion Q as [| r R]; subst.
  pose proof (divisor_range 1 2 R) as Range2.
  destruct Range2 as [R3 | R4].
  symmetry in R3.
  pose proof (O_S 0); contradiction.

  repeat (apply le_S_n in R4); apply Le.le_n_0_eq in R4.
  pose proof (O_S 0); contradiction.
Qed.

Lemma zero_divide k : Divides 0 k -> k = 0.
  intro D.
  induction D; auto; auto.
Qed.

Theorem five_prime :
  Prime 5.
Proof.
  intros k D.
  pose proof (divisor_range 5 k D) as Range.
  destruct Range as [|Bound]; [congruence|].

  (* Handle k=5. *)
  inversion Bound as [KE5 | k1 KLE4].
  auto. subst.

  (* Handle k=4 (contradiction). *)
  inversion KLE4 as [KE4 | k1 KLE3].
  subst.
  pose proof four_doesnt_divide_five; contradiction.
  subst.

  (* Handle k=3 (contradiction). *)
  inversion KLE3 as [KE3 | k1 KLE2].
  subst.
  pose proof three_doesnt_divide_five; contradiction.
  subst.

  (* Handle k=2 (contradiction). *)
  inversion KLE2 as [KE2 | k1 KLE1].
  subst.
  pose proof two_doesnt_divide_five; contradiction.
  subst.

  (* Handle k=1. *)
  inversion KLE1 as [KE1 | k1 KLE0].
  auto.
  subst.

  (* Handle k=0. *)
  inversion KLE0 as [KE0 |].
  subst.
  pose proof (zero_divide 5 D); auto.
Qed.