proposition: Lemma test_have n : reflect (exists x y z, x ^ n + y ^ n == z ^ n) ((n == 1) || (n == 2)).
proof: Proof. have test0 : forall x y z, x ^ 0 + y ^ 0 != z ^ 0 by []. have test1 : exists x y z, x ^ 1 + y ^ 1 = z ^ 1 by exists 0, 0, 0. have test2 : exists x y z, x ^ 2 + y ^ 2 = z ^ 2 by exists 3, 4, 5. suff test m : m >= 3 -> forall x y z, x ^ m + y ^ m != z ^ m. case: n => [|[|[|n]]]//=; constructor. - by move=> [x [y [z]]]; rewrite (negPf (test0 _ _ _)). - by have [x [y [z /eqP]]] := test1; exists x, y, z. - by have [x [y [z /eqP]]] := test2; exists x, y, z. - by move=> [x [y [z]]]; rewrite (negPf (test _ _ _ _ _)). Abort. Lemma prime_above (m : nat) : exists p, (prime p) && (m < p). Proof. have: 1 < m`! + 1 by rewrite addn1 ltnS fact_gt0. move=> /pdivP[q pr_q q_dv_m1]. exists q; rewrite pr_q /= ltnNge. apply: contraL q_dv_m1 => q_le_m. by rewrite dvdn_addr ?dvdn_fact ?prime_gt0 // gtnNdvd ?prime_gt1. Qed.
imports: mathcomp(all_ssreflect)