Ssreflect Users Discussion List

[Laurent Théry <>]

On 04/01/2014 11:46 AM, bertot wrote:
> Dear all,
>
> I am amazed that we cannot find a proof that there are an infinity of 
> prime numbers in the Math. Comp. library.  Do you have one, that you 
> will be willing to share?  Could it be possible that there was one in 
> a previous version, which could have been removed in one of our 
> re-factoring steps?
>
> Yves

Before Georges one liner ;-)

Lemma fact_div m n : 0 < m <= n -> m %| n`!.
Proof.
elim: n m => [[] //| /= n IH m].
rewrite factS [_ <= _.+1]leq_eqVlt; case: eqP => /= => [-> //| _ /IH H].
  by rewrite dvdn_mulr.
by rewrite dvdn_mull.
Qed.

Lemma prime_inf m : {p | m < p & prime p}.
Proof.
pose c := pdiv m`!.+1.
have Pc : prime c by apply/pdiv_prime/fact_gt0.
exists c => //.
have [cLm|//] := leqP.
have /Euclid_dvd1 := Pc.
have /eqP<- := coprimenS (m`!).
rewrite dvdn_gcd pdiv_dvd.
by have /fact_div-> : 0 < pdiv m`!.+1 <= m by rewrite prime_gt0.
Qed.