proposition: Lemma CS_finite_o x: finite_o x -> cardinalp x.
proof: Proof. move => h; case: (equal_or_not x \0c); first by move => ->; apply: CS0. by move/(finite_pred h) => [y yF ->]; apply: CS_osucc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)