proposition: Lemma ord_epsilon_p13 a x: ordinalp a -> ordinalp x -> (a ^o x = x) -> ( (a <o omega0 -> ((a = \1o /\ x = \1o) \/ (\2o ^o x = x))) /\ (omega0 <=o a -> (epsilonp x /\ a <o x))).
proof: Proof. move => oa ox h. have pa: \2o <=o a -> \2o ^o x = x. move => a2; apply: oleA. by move: (opow_Mleeq card2_nz a2 ox); rewrite h. by move: (opow_Mspec (oleR OS2) ox). case: (equal_or_not x \0o) => xnz. by case:(proj2 olt_01); move: h; rewrite xnz opowx0. split => ao. case: (ord2_trichotomy oa) => az. - by move: h; rewrite az opow0x => h0; case: xnz. - by left;split => //; rewrite -h az opow1x. - by right; apply: pa. have a2:=(oleT (ole_2omega) ao). have h1:= (pa a2). have x2 : \1o <o x. split; first by apply:oge1. move => x1; move: h1; rewrite - x1 (opowx1 OS2); exact (nesym(proj2 olt_12)). move: (opow_Meqlt a2 x2); rewrite (opowx1 oa) h => ax. move: (proj2(ole_ltT ao ax)) => xo. split; last by exact. case:(ord_epsilon_p11 ox h1); [ by move => xno; case: xo | exact]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)