proposition: Lemma ord_epsilon_p9 x a: epsilonp x -> a <o x-> [/\ a +o x = x, (\1o <=o a -> a *o x = x) & (\2o <=o a -> a ^o x = x) ].
proof: Proof. move=> oex lax. have oox:=(ord_eps_p3 oex). have [ox xx] := oex. have pa: forall n, \1o <=o n -> n <o x -> n *o x = x. move: (critical_productP x) => [_ pb]. have: (exists2 n, ordinalp n & x = oopow (oopow n)). by exists x => //;rewrite xx xx. move /pb => [_ _ pd] //. split. by apply: indecomp_prop1 lax; rewrite -xx; apply: indecomp_prop4. by move=> a1;apply: pa a1 lax. move: OS_omega => oo a2. have oa:= proj32 a2. have [lt1o _] := olt_1omega. have oxx:= (pa _ lt1o oox). rewrite - {1} oxx (opow_prod oa oo ox). case: (oleT_el oo oa) => coa; last first. by rewrite (opow_int_omega a2 coa). have ap:=(olt_leT olt_02 a2). rewrite - xx in lax. move: (the_cnf_p6 ox ap lax) => h2. have od:=(proj31_1 h2). move/oge1P:(odegree_infinite coa) => gd1. rewrite (CNF_pow_pr3 coa) - (opow_prod oo (OS_prod2 od oo) ox). by rewrite -(oprodA od oo ox) (pa _ lt1o oox) (pa _ gd1 h2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)