proposition: Lemma card_dominant_pr12 x: infinite_c x -> (forall m, infinite_c m -> m <c x -> \2c ^c m <c x) -> card_dominant x.
proof: Proof. move => icx ha; apply:(card_dominant_pr1 (proj1 icx) (infinite_nz icx)). move => m lmx. case: (finite_or_infinite (proj31_1 lmx)) => li; last by apply:ha. by apply:clt_fin_inf icx; apply/NatP; apply:(NS_pow NS2); apply/NatP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)