proposition: Lemma nat_prime_p7 a: natp a -> \1c <=c a -> exists p n, [/\ nat_factor_list p n, natp n & oprodf p n = 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 => m mN Hrec a am. case:(cle_eqVlt am) => lekn; last by move/(cltSleP mN): lekn; apply:Hrec. move => le1a. case: (equal_or_not \1c a) => ea1. exists (fun z => \0c), \0c; split; [ | exact: NS0 |by rewrite oprod_f0 ]. split; [ by move => i /clt0 | by move => i /clt0 | by move => i _ /clt0]. move: (nat_prime_p3 (NS_le_nat am (NS_succ mN)) (conj le1a ea1)) => [y npy yda]. pose pr y := nat_prime y /\ y %|c a. have oy :=(OS_nat (proj31 npy)). have pry: pr y by []. move:(least_ordinal4 oy pry); set z := least_ordinal _ _. move => [oz [npz zda] lz]; move:(npz) => [zN lt1z zpr]. move: (cdivides_pr zda) (NS_quo z (proj31 zda)); set q := (a %/c z)=> av qN. move:(le1a); rewrite av => /(cprod_ge1 zN qN) [_ le1q]. have leqm: q <=c m. apply/(cltSleP mN);rewrite - lekn av cprodC; exact:(cprod_M1lt' qN le1q lt1z). move: (Hrec q leqm le1q) =>[p [n [nflp nN poq]]]. pose p' i := Yo (i <c n) (p i) z. have eq0: p' n = z by rewrite /p' (Y_false (cleNgt (cleR (CS_nat nN)))). have eq1: oprodf p' n = oprodf p n. by apply: (oprodf_exten nN) => i lin; rewrite /p'; Ytac0. have eq2:oprodf p' (csucc n) = z *c q. by rewrite (oprod_fS _ nN) eq1 poq eq0 (oprod2_2int qN zN) cprodC. exists p', (csucc n); split; [ | apply: (NS_succ nN) | done]. split. - move => i /(cltSleP nN) lin; case: (cle_eqVlt lin) => ltin. by rewrite ltin eq0. rewrite /p' (Y_true ltin); exact: (proj31 nflp _ ltin). - move => i /(cltSleP nN) lin; case: (cle_eqVlt lin) => ltin. by rewrite ltin eq0. rewrite /p' (Y_true ltin); exact: (proj32 nflp _ ltin). - move => i iN /(cltSleP nN) lesin. move:(clt_leT (cltS iN) lesin) => ltin. rewrite {2}/p' (Y_true ltin). case: (cle_eqVlt lesin) => lesin';last first. rewrite /p' (Y_true lesin'); exact: (proj33 nflp _ iN lesin'). rewrite lesin' eq0. move: (cdivides_trans2 zN (nat_prime_p4 nN nflp ltin)). rewrite cprodC poq -av => pida. move: (proj32 nflp _ ltin) => pip. by apply: (lz (p i) (OS_nat (proj31 pip))); split. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)