proposition: Lemma ord_factor8 p n i: ofact_list_succ p n -> i <c n -> nat_prime (p i) \/ [/\ ordinalp (p i), ~(natp (p i))& p i = osucc (oopow (odegree (p i)))].
proof: Proof. move =>[[_ h1 _] h2] lin. case/ord_prime_p1:(h1 _ lin). - by left. - move => h3; right. move/ord_ptypeI_prop: (h3) => [_ cp]; move:(proj32 cp) => op. split => //; first by move/olt_omegaP; case/oltNge. by case: h3 => d dp ->; rewrite (odegree_succ_pow dp). - move/ord_ptypeL_prop => [lp _]. case (limit_nonsucc' lp (h2 _ lin)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)