proposition: Lemma CIS_pow3 x y : \2c <=c x -> infinite_c y -> infinite_c (x ^c y).
proof: Proof. move => sa sb. have sc:= (cpow_Mleeq y sa card2_nz). exact:(cle_inf_inf sb (cleT (proj1 (cantor (proj1 sb))) sc)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)