proposition: Lemma CS_osucc x: finite_o x -> cardinalp (osucc x).
proof: Proof. move=> [ox nix]; apply/cardinalP; split; first by apply: OS_succ. move=> z zo [f fp]; case:nix. apply: EqT (EqS (equipotent_bp fp)). have zx: (sub z x) by move/(oleP ox): zo => /proj33. apply:CantorBernstein. have aux: sub x (osucc x) by rewrite /osucc; fprops. exists (restriction f x); exact:(restriction_fi aux fp). exists (canonical_injection z x); rewrite/canonical_injection;saw. by apply: ci_fi. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)