proposition: Lemma card_dominant_pr1 x: cardinalp x -> x <> \0c -> (forall m, m <c x -> \2c ^c m <c x) -> card_dominant x.
proof: Proof. move=> cx xnz h. have ix: infinite_c x. case: (finite_or_infinite cx) => // fx. have xN: natp x by apply /NatP. move: (cpred_pr xN xnz) => [pa pb]. have pc: (cpred x) <c x by rewrite {2} pb; apply: cltS. move: (h _ pc); rewrite {2} pb; move /(cltSleP pa) => h1. case: (cleNgt h1 (cantor (proj32 h1))). split => //. move=> a b ax bx. case: (equal_or_not b \0c) => bz. rewrite bz cpowx0; apply: clt_fin_inf => //. rewrite /NatP; fprops. case: (equal_or_not a \0c) => az. rewrite az cpow0x // ; apply: clt_fin_inf => //. rewrite /NatP; fprops. have [c [ca cb ccx]]: exists c, [/\ a <=c c, b <=c c & c <c x]. have ca:= proj31_1 ax. have cb:= proj31_1 bx. case: (cleT_ee ca cb); [ exists b; split | exists a;split ]; fprops. have h1 : a ^c b <=c c ^c c by apply: cpow_Mlele. apply (cle_ltT h1). case: (finite_or_infinite (proj31_1 ccx)) => fc. apply: clt_fin_inf => //. by apply /NatP; apply NS_pow; apply /NatP. by rewrite (infinite_power1_b fc); apply h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)