proposition: Lemma critical_product_pr3 a b: \1o <o a -> \1o <o b -> indecomposable b -> critical_ordinal \1o oprod2 (a ^o b).
proof: Proof. move=> a1 b1 bi. have ob:= proj32_1 b1. move: (indecomp_prop3 bi) => [c oc bv]. apply/(proj2 (critical_productP (a ^o b))). suff: exists m, [/\ ordinalp m,indecomposable m& a ^o b = omega0 ^o m]. move=> [m [om im ->]]. move: (indecomp_prop3 im) => [n nc -> ]. by exists n. case:(ozero_dichot oc) => cp. by move: b1; rewrite bv cp oopow0; move => []. have blim: limit_ordinal b. by case: (indecomp_limit bi) => // e1; case: (proj2 b1). have aux t : \0o <o t -> indecomposable (t *o b). by move => tp;move/(indecomp_prodP b1 tp): bi. have x2: \2o <=o a by apply /oge2P. have oa:= proj32 x2. case: (oleT_el OS_omega oa) => fina. rewrite(CNF_pow_pr4 fina blim). have dp := (odegree_infinite fina); have od := (OS_prod2 (proj32_1 dp) ob). exists (odegree a *o b); split => //. by apply/(indecomp_prodP b1 dp). move: (CNF_pow_pr5 x2 fina blim) => [z [oz sb sc]]; exists z; split => //. case: (ozero_dichot oz)=> zp. by case: (proj2 (proj1 bi)); rewrite sb zp oprod0r. case: (equal_or_not \1o z) => ez1; first by rewrite - ez1; exact: indecomp_one. have z1: \1o <o z by split; [ apply/oge1P | ]. apply /(indecomp_prodP z1 olt_0omega); ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)