proposition: Lemma nat_prime_factor_vS p n: natp n -> nat_factor_list p (csucc n) -> [/\ natp (oprodf p n), natp (p n) & oprodf p (csucc n) = (oprodf p n) *c (p n)].
proof: Proof. move => nN H. move: (NS_nat_prime_factor nN (nat_factor_list_rec nN H)) => fN. move:(proj31 (proj32 H _ (cltS nN)))=> pN. by rewrite (oprod_fS _ nN) (oprod2_2int fN pN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)