proposition: Lemma CNF_pow_pr5_deg x y: \2o <=o x -> x <o omega0 -> ordinalp y -> odegree (x ^o y) = oquo y omega0.
proof: Proof. move => lx2 lxo oy. move: (oquoremP oy olt_0omega); set q := oquo _ _; set r := orem _ _. move =>[oq or -> rs]. move: (proj32 lx2) (olt_leT olt_02 lx2) (OS_prod2 OS_omega oq) => ox xp op. rewrite (opow_sum ox op or). rewrite (opow_prod ox OS_omega oq) (opow_int_omega lx2 lxo). rewrite (odegree_prod (oopow_pos oq) (opow_pos xp or)). rewrite (odegree_opow oq). by rewrite (odegree_finite (opow_2int1 lxo rs)) (osum0r oq). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)