proposition: Lemma NS_nat_prime_factor p n: natp n -> (nat_factor_list p n) -> natp (oprodf p n).
proof: Proof. move => nN [_ H _]. have: forall i, i<c n -> natp (p i) by move => i /H []. clear H; move: n nN; apply: Nat_induction. by move => _;rewrite oprod_f0; apply: NS1. move => n nN Hr fn1; rewrite (oprod_fS _ nN). move: (true_below_rec nN fn1) => [ha hb]. have hc:=(Hr ha); rewrite (oprod2_2int (Hr ha) hb); fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)