Require Pocklington.

Lemma prime3: (Prime (3)).
Proof.
   Apply (Zpocklington `3` `2` `1` `2` (Cons nat (2) (Nil nat))).
   Unfold Zgt. Simpl. Reflexivity.
   Unfold Zle. Simpl. Discriminate.
   Unfold Zle. Simpl. Discriminate.
   Change `3=3`. Reflexivity.
   Change `2=2`. Reflexivity.
   Unfold allPrime. Simpl.
   Split. Exact prime2.
   Trivial.
   Replace (Zminus `3` `1`) with `2`.
   Simpl. Split with `1`.    Change `4=4`. Reflexivity.
   Change `2=2`. Reflexivity.
   Unfold ZallLinCombMod.
   Split. Unfold LinCombMod.
   Split with `1`. Split with `0`.
   Apply mod_trans with (Zplus (Zmult (Zminus `2` `1`) `1`) (Zmult `3` `0`)).
   Simpl. Split with `0`.    Change `1=1`. Reflexivity.
   Apply mod_plus_compat.
   Apply mod_mult_compat.
   Apply mod_minus_compat.
   Apply mod_sym.
   Rewrite (zexp_eq (Zmult `1` (inject_nat (multDrop (2) (Cons nat (2) (Nil nat))))) `1`).
   Simpl. Split with `0`.    Change `2=2`. Reflexivity.
   Change `1=1`. Reflexivity.
   Apply mod_refl. Apply mod_refl. Apply mod_refl.
   Simpl. Trivial.
   Unfold Zle. Simpl. Discriminate.
Qed.