proposition: Lemma finite_c_P2 x: finite_c x <-> (x <c omega0).
proof: Proof. split; last by move => /oclt/olt_i /omega_P2. move => fa. apply: (oclt3 (CS_finite fa) CS_omega). by apply/(oltP OS_omega); apply/omega_P2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)