proposition: Lemma CNF_pow_pr5 x y: \2o <=o x -> x <o omega0 -> limit_ordinal y -> exists z, [/\ ordinalp z, y = omega0 *o z & x ^o y = oopow z].
proof: Proof. move=> x2 xo limy. move/ (limit_ordinal_P4 (proj31 limy)): limy => [z /proj32_1 oz ->]. by rewrite (opow_prod (proj32 x2) OS_omega oz) (opow_int_omega x2 xo); exists z. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)