proposition: Lemma ord_epsilon_p11 x: ordinalp x -> (\2o ^o x = x) -> x = omega0 \/ epsilonp x.
proof: Proof. move=> ox hx. move: (oquoremP ox olt_0omega). set q := oquo _ _; set r := orem _ _ ; move=> [oq or av bv]. have le22:=oleR (OS2). have oo:= OS_omega. case: (equal_or_not r \0o) => rnz; last first. have rN: natp r by apply /olt_omegaP. move: (cpred_pr rN rnz) => [pb pv]. have op := (OS_nat pb). move: av; rewrite pv (succ_of_nat pb) - (osum2_succ (OS_prod2 oo oq) op). set v := (omega0 *o q) +o cpred r => xs. have ov: ordinalp v by rewrite /v; fprops. case: (ozero_dichot ov) => vz. by case: (proj2 olt_12); move: hx; rewrite xs vz osucc_zero (opowx1 OS2). have o2v: ordinalp (\2o ^o v) by fprops. move: hx; rewrite xs (opow_succ OS2 ov) (ord_double o2v) => h. move: (osum_Mlele (opow_Mspec le22 ov) (opow_Meqle1 olt_02 vz)). rewrite h - (osucc_pr ov). by move/(osum_Meqler OS2 OS1 ov) => /(oltNge olt_12). move: av; rewrite rnz (osum0r (OS_prod2 oo oq)). move => xq; case: (ozero_dichot oq) => qz. move: hx; rewrite xq qz oprod0r opowx0 => h1. by symmetry in h1; move: olt_01 => [_] h2. case: (equal_or_not \1o q) => qo. by left;rewrite xq -qo (oprod1r); fprops. right. have o2:= olt_2omega. move: hx; rewrite xq (opow_prod OS2 oo oq) (opow_int_omega le22 o2). move: (ord_rev_pred qz); set y:= (q -o \1o); move => [yo yv]. rewrite yv (opow_sum oo OS1 yo) (opowx1 oo) => pa. have ooy: ordinalp (omega0 ^o y) by fprops. have o1y: ordinalp (\1o +o y) by rewrite - yv. move: (oprod2_simpl ooy o1y olt_0omega pa). move: (opow_Mspec ole_2omega yo) => pc res1. symmetry in res1. case: (indecomp_pr OS1 yo (indecomp_prop4 yo) res1); rewrite /oopow => eq1. by move: qo; rewrite yv res1 -eq1. by rewrite res1- {1} [omega0] (opowx1 oo) -(opow_sum oo OS1 yo) res1 -eq1 -eq1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)