proposition: Lemma cofinality_limit3 x: limit_ordinal x -> limit_ordinal (\cf x).
proof: Proof. move => [pa pb pc]. case: (cofinality_limit2 pa). have xnz: x <> emptyset by move =>h; move: pb; rewrite h; case; case. by move: (cofinality_n0 pa xnz). case => //. rewrite (cofinality_limit1 pa); move => [m om xs]. have mx: inc m x by rewrite xs /osucc; fprops. by move: (pc _ mx); rewrite -xs => xx; case: (ordinal_decent pa xx). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)