proposition: Lemma card_dominant_pr5 x: card_dominant x -> (\2c ^<c x = x /\ \2c ^c x = gimel_fct x).
proof: Proof. move => [icx cdx]. suff pa: \2c ^<c x = x. split; [ by exact | by rewrite (cpow_less_pr6a icx) pa ]. move: (icx) => [cx _]. have aux:= (@cpow_less_pr0 \2c x). apply: cleA. apply:card_ub_sup => //i /funI_P [z zi ->]. have pa:=(clt_fin_inf finite_2 icx). move: zi => /(cardinals_ltP cx) pb. exact (proj1 (cdx _ _ pa pb)). by case: (cpow_less_compare icx). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)