proposition: Lemma cpow_less_pr6 x z: infinite_c x -> \2c <=c z -> z ^c x = (z ^<c x ) ^c (\cf x).
proof: Proof. move => icx t2. move: (cofinality_c_pr3 icx) => [f [ [[pa1 pa2 pb pc] pd] _]]. apply: cleA. rewrite - (cofinality_card icx) -{1} pd (cpow_sum _ f). rewrite - pc - cprod_of_same /cst_graph; aw. apply: cprod_increasing; aww => t td; rewrite !LgV//. by apply: cpow_less_pr2; apply: pb. have tp:=(clt_leT clt_02 t2). have h:= (cpow_less_pr1 tp (proj1 icx)). have cnz:= (infinite_nz (cofinality_infinite_cardinal icx)). case: (equal_or_not (z ^<c x) \0c) => aux. by rewrite aux (cpow0x cnz); apply: (cle0x (proj32 h)). move: (cpow_Mleeq (\cf x) h aux). by rewrite - cpow_pow (cprod_inf (cofinality_small icx) icx cnz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)