proposition: Lemma CNF_pow_pr3 x: omega0 <=o x -> x ^o omega0 = oopow ((odegree x) *o omega0).
proof: Proof. move => xinf. have oo:= OS_omega. move:(olt_leT olt_0omega xinf) => xp. move:(odegree_infinite xinf) => enz; move: (proj32_1 enz) => oe. move:(the_cnf_p4 xp) => [le1 le2]. have od := proj32_1 xp; have pa:= (oopow_pos od). move:(opow_Mleeq (oopow_nz oe) le1 OS_omega). move:(opow_Mleeq (nesym (proj2 xp)) (proj1 le2) OS_omega). rewrite - (opow_prod oo (OS_succ oe) oo) - (opow_prod oo oe oo). rewrite(indecomp_prod3 enz); apply: oleA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)