proposition: Lemma CNF_pow_pr1_bis x k: limit_ordinal x -> natp k -> x ^o (osucc k) = (oopow ((odegree x) *o k)) *o x.
proof: Proof. move/ovaluation3_rev => [xp vxp] kN. move:(the_cnf_p0_nz xp) => [qa qb]. by move:(CNF_pow_pr1 qa vxp kN); rewrite (odegree_of_pos xp) qb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)