proposition: Lemma cpow_less_compare x: infinite_c x -> (x <=c \2c ^<c x /\ \2c ^<c x <=c x ^<c x /\ x ^<c x <=c x ^c x).
proof: Proof. move => icx; move: (proj1 icx) => cx. have x2:= (infinite_ge2 icx). split. move: (@cpow_less_pr0 \2c x) => aux. case: (cleT_el cx (CS_cpow_less \2c x)) => // pa. set u := \2c ^<c x. have le : \2c ^c u <=c u. apply: card_sup_ub => //; apply /funI_P;exists u => //. apply /cardinals_ltP => //. case: (cleNgt le (cantor (proj31_1 pa))). split. apply: card_sup_image; move=> t tx; apply: (cpow_Mleeq _ x2);fprops. apply: cpow_less_pr1 => //; split; first by apply: cle0x. exact: (nesym (infinite_nz icx)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)