proposition: Lemma cpow_less_pr7b x (y := cnext x) : infinite_c x -> csumb (cardinals_lt y) (fun t => y ^c t) = \2c ^c x.
proof: Proof. move => icx; move: (icx) => [cx _]. have pa:=(cnext_pr2 cx). have iy:= (cle_inf_inf icx (proj1 pa)). have y2:= (infinite_ge2 iy). have qa:= (clt_leT clt_02 y2). rewrite - (cpow_less_alt iy y2). by rewrite (cpow_less_pr4 qa icx) infinite_power1 //; apply: cnext_pr3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)