proposition: Lemma nat_prime_p5 p n q: natp n -> (nat_factor_list p n) -> nat_prime q -> q %|c (oprodf p n) -> exists2 i, i <c n & q = p i.
proof: Proof. move => nN h qp; move: n nN h; apply: Nat_induction. rewrite oprod_f0; move: qp => [_ [_ q1] _] _ /cdivides_oner nq1. by case:q1. move => n nN Hrec hsn. move:(nat_prime_factor_vS nN hsn) => [fN pnN ->] qdv. case: (nat_prime_coprime qp (proj32 hsn _ (cltS nN)))=> cpd. exists n => //; exact: (cltS nN). move:(Hrec(nat_factor_list_rec nN hsn) (coprime3 cpd fN qdv)). move => [i lin ->];exists i => //; exact: (clt_ltT lin (cltS nN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)