proposition: Lemma nat_prime_p3 a: natp a -> \1c <c a -> exists2 p, nat_prime p & p %|c a.
proof: Proof. move => aN;move: (cleR (CS_nat aN)); move: a aN {1 3 4}a; apply:Nat_induction. move => a /cle0 -> [/cleNgt[]]; exact:clt_01. move => n nN Hrec a alesn lt1a. have aN:=(NS_le_nat alesn (NS_succ nN)). case: (p_or_not_p (composite a)); last first. by move/(nat_prime_p2 aN lt1a);exists a => //; apply: cdivides_itself. move => [b [bN lt1b ltba bda]]. move/(cltSleP nN):(clt_leT ltba alesn) => lebn. by move:(Hrec _ lebn lt1b) => [p pa /(cdivides_trans bda) pb]; exists p. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)