proposition: Lemma prime_above m : exists2 p, m < p & prime p.
proof: Proof. have /pdivP[p pr_p p_dv_m1]: 1 < m`! + 1 by rewrite addn1 ltnS fact_gt0. exists p => //; rewrite ltnNge; apply: contraL p_dv_m1 => p_le_m. by rewrite dvdn_addr ?dvdn_fact ?prime_gt0 // gtnNdvd ?prime_gt1. Qed.
imports: mathcomp(all_ssreflect)