proposition: Lemma infinite_c_P2 x: infinite_c x <-> (omega0 <=c x).
proof: Proof. move: CS_omega => h; split. by move=> [pa pb]; split => //; apply /(omega_P1 (OS_cardinal pa)). by move=> [pa pb pc]; split => //; apply /(omega_P1 (OS_cardinal pb)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)