proposition: Lemma cofinality_limit1 n: ordinalp n -> ((\cf n = \1o) <-> exists2 m, ordinalp m & n = osucc m).
proof: Proof. move => on; split; last first. move=> [m om ->]; rewrite cofinality_succ //. move => fc1. move: (cofinality_rw on) => [_ [f [[ff sf tf] cf]] _]. move: sf cf; rewrite fc1 / \1o / \1c => sf cf. set m := Vf f emptyset. have mn: inc m n by rewrite -tf; apply: Vf_target => //; rewrite sf;fprops. move: (Os_ordinal on mn) => om. exists m => //. case :(oleT_ell on (OS_succ om)) => //. by move: mn => /(oltP on) pa /oltSleP => /(oltNge pa). move /(oltP on) => /cf [z] /set1_P. rewrite -/m;move=> -> h1;case: (oltNge (oltS om) h1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)