proposition: Lemma CNF_pow_pr4 x y: omega0 <=o x -> limit_ordinal y -> x ^o y = oopow ((odegree x) *o y).
proof: Proof. move: OS_omega => oo infx limy. have ox:= proj32 infx. have op := (OS_degree (proj32 infx)). move/ (limit_ordinal_P4 (proj31 limy)): limy => [z /proj32_1 oz ->]. rewrite (opow_prod ox oo oz) (CNF_pow_pr3 infx). by rewrite - (opow_prod oo (OS_prod2 op oo) oz) (oprodA op oo oz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)