proposition: Lemma infinite_power4 a (b:= \2c ^c a): infinite_c a -> [/\ b ^c a = b, b ^c a <c (cnext b) ^c a, (forall c, \2c <=c c -> c ^c a = c -> b <=c c) & (forall c, infinite_c c -> c ^c a <c (cnext c) ^c a -> b <=c c)].
proof: Proof. move=> ica. have anz: a <> \0c by apply: infinite_nz. have ib: infinite_c b by apply: infinite_pow2. have p1: b ^c a = b by rewrite/b - cpow_pow csquare_inf. have p3: (forall c, \2c <=c c -> c ^c a = c -> b <=c c). move =>c c2 cp. have cc:=proj32 c2. case: (cleT_el (proj1 ib) cc) => //; move=> [le1 ne1]. move: (infinite_power1 c2 le1 ica); rewrite cp -/b //. have p2: b ^c a <c cnext b ^c a. move: (proj32 (cnext_pr1 (proj1 ib))). rewrite (infinite_power2_bis ib anz) p1 => h; move: (proj1 h) => le1. move: (infinite_nz ib) => bnz. have isc: infinite_c (cnext b) by apply: (cle_inf_inf ib le1). by rewrite cprodC (cprod_inf le1 isc bnz). split => //. move=> c ic; rewrite (infinite_power2_bis ic anz) => ha. have c1: cardinalp (c ^c a) by fprops. have c2 := (CS_cnext (proj1 ic)). case: (cleT_el c2 c1) => h. have ip: infinite_c (c ^c a) by apply: CIS_pow2. by move: (cleNgt (cprod_inf1 h ip) ha). move: (cnext_pr4 (proj1 ic) h) => h1. apply: (p3 _ (infinite_ge2 ic)). apply: cleA => //; apply: (cpow_Mle1 (proj32 h1) anz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)