proposition: Lemma infinite_card_limit2 x: infinite_c x -> limit_ordinal x.
proof: Proof. move => ic; move: (ic) => [p1 p2]. apply/(limit_ordinal_P0 (proj1 (proj1 ic))). split; last by apply: infinite_card_limit1. by apply/nonemptyP; apply: infinite_nz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)