proposition: Lemma nat_prime_p2 a: natp a -> \1c <c a -> (nat_prime a <-> ~ composite a).
proof: Proof. move => aN ag1; split. move => [_ _ ap] [b [bN [le1b /nesym n1b] [_ lba] bda]]. move: (cdivides_pr bda) => av. case(ap _ _ bN (NS_quo b aN) av) => // eq1. case: lba; rewrite av eq1 cprod1r; fprops. move => nca; split => // b c bN cN eq1. move: (proj1 ag1); rewrite eq1 => /(cprod_ge1 bN cN) [le1b le1c]. case:(cle_eqVlt le1b) => lt1b; first by left. case:(cle_eqVlt le1c) => lt1c; first by right. have lba: b <c a by rewrite eq1; apply:(cprod_M1lt' bN le1b lt1c). move:(cdivides_pr1 cN bN); rewrite - eq1 => bdp. by case: nca; exists b. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)