proposition: Lemma nat_factor_list_rec p n: natp n -> nat_factor_list p (csucc n) -> nat_factor_list p n.
proof: Proof. move => nN [ha hb hc]. have H i: i<c n -> i <c (csucc n) by move => lin;apply: clt_ltT (cltS nN). split => //. - by move => i /H /ha. - by move => i /H /hb. - by move => i iN /H lsin; apply:(hc i iN lsin). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)