proposition: Lemma CNF_pow_pr4_deg x y: omega0 <=o x -> ordinalp y -> odegree (x ^o y) = odegree x *o y.
proof: Proof. move => xgo oy. move: (oquoremP oy olt_0omega); set q := oquo _ _; set r := orem _ _. move =>[oq or -> rs]. move: (proj32 xgo) (olt_leT olt_0omega xgo) (OS_prod2 OS_omega oq) => ox xp op. have od := (OS_degree ox). have op1:= (OS_prod2 od OS_omega). rewrite (opow_sum ox op or) (odegree_prod (opow_pos xp op)(opow_pos xp or)). rewrite (opow_prod ox OS_omega oq) (CNF_pow_pr3 xgo). rewrite - (opow_prod OS_omega op1 oq) (odegree_opow (OS_prod2 op1 oq)). suff: odegree (x ^o r) = (odegree x) *o r. by move ->; rewrite - (oprodA od OS_omega oq) (oprodD op or od). move/olt_omegaP: rs; clear or;move: r; apply: Nat_induction. by rewrite opowx0 oprod0r odegree_one. move => n nN; move:(OS_nat nN) => on. rewrite (succ_of_nat nN) (opow_succ ox on) (oprod2_succ od on). by rewrite (odegree_prod (opow_pos xp on) xp) => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)