proposition: Lemma cpow_less_alt x y : infinite_c y -> \2c <=c x -> x ^<c y = csumb (cardinals_lt y) (fun t => x ^c t).
proof: Proof. move=> icy xy. rewrite /cpow_less; set E := (cardinals_lt y). set f := (Lg E [eta cpow x]). have cf: cardinal_fam f by rewrite/f;hnf;aw => t te; rewrite LgV//; fprops. set s:= (union (range f)). have <-: s = union (fun_image E (cpow x)) by rewrite /s Lg_range. have cy:=(proj1 icy). move: (infinite_power7d cy (infinite_nz icy)); rewrite -/E; move => [pw _]. suff aux: y <=c s. symmetry; apply: csum_of_small_b4; fprops. - apply: (cle_inf_inf icy aux). - by move: (cleT pw aux); aw. have fgf: fgraph f by rewrite /f; fprops. have csr: cardinal_set (range f). move => t /(range_gP fgf); rewrite /f;aw;move => [z ze ->]; rewrite LgV//; fprops. case: (cleT_el cy (CS_sup csr)) => //; rewrite -/s => sy. move: (cantor (CS_sup csr)); rewrite -/s => /cltNge; case. have sE: inc s E by apply /(cardinals_ltP cy). apply: (cleT (cpow_Mleeq s xy card2_nz)). apply: card_sup_ub => //; apply /(range_gP fgf). by rewrite /f; aw;ex_tac; rewrite LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)