proposition: Lemma cofinality_limit2 x (y:= \cf x): ordinalp x -> y = \0o \/ y = \1o \/ limit_ordinal y.
proof: Proof. move=> ox; move: (cofinality_rw ox) => [oy pb pc]. case: (equal_or_not x \0o) => xnz. by rewrite /y xnz cofinality0; left. case: (ordinal_limA oy); [by left | | by right; right ]. rewrite -/y; move=> [a oa ca]; right; left. move: pb => [f [[ff sf tf ] cf]]. have ay: inc a y by rewrite ca /osucc; fprops. have ay1: a <o y by apply /oltP. have fax: inc (Vf f a) x by rewrite - tf; apply:Vf_target => //; ue. have ow: ordinalp (Vf f a) by apply: (Os_ordinal ox). case: (p_or_not_p (exists2 b, inc b a & Vf f a <=o Vf f b)) => h2. suff cfa: cofinal_function_ex x a. case move:(oltNge ay1 (pc _ oa cfa)). move: (ordinal_transitive oy ay); rewrite - sf => saf. exists (restriction f a). split. split => //; rewrite /restriction; aw; trivial. apply: (proj31(restriction_prop ff saf)). move => t tx; move: (cf _ tx) => [z ]; rewrite -/y ca => zs tv. case /setU1_P: zs => za; first by ex_tac; rewrite restriction_V //. move: h2 => [b ba le]; ex_tac. rewrite za in tv; rewrite restriction_V //; exact:(oleT tv le). suff: x = osucc(Vf f a) by rewrite /y; move ->; apply:cofinality_succ. set_extens t. move => tx; move: (cf _ tx) => [z zy tz]; apply/(oleP ow). case: (equal_or_not z a) => za; first by ue. have iza: inc z a. apply /(oltP oa); split => //. by apply /oltSleP; rewrite - ca; apply /(oltP oy). case: (oleT_ee ow (proj32 tz)) => xx;[ case: h2; ex_tac | exact: oleT tz xx]. move/(oltP ox):fax => lt1. by move/(oleP ow) => le1; apply/(oltP ox); apply:(ole_ltT le1 lt1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)