proposition: Lemma nat_prime_p4 p n i: natp n -> (nat_factor_list p n) -> i <c n-> p i %|c (oprodf p n).
proof: Proof. move => nN; move: n nN i; apply:Nat_induction;first by move => i _ /clt0. move => n nN Hrec i hr/(cltSleP nN) lin. move:(nat_prime_factor_vS nN hr) => [fN pnN ->]. case:(cle_eqVlt lin) => ltin. by rewrite ltin cprodC; apply: (cdivides_pr1 fN pnN). exact:(cdivides_trans2 pnN (Hrec i (nat_factor_list_rec nN hr) ltin)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)