proposition: Lemma infinite_power1 a b: \2c <=c a -> a <=c (\2c ^c b) -> infinite_c b -> a ^c b = \2c ^c b.
proof: Proof. move=> le1 le2 ic. have bb:= (cleR (proj1 ic)). have ap:= nesym (proj2 (clt_leT clt_02 le1)). move: (cpow_Mlele ap le2 bb)(cpow_Mlele card2_nz le1 bb). rewrite - cpow_pow (csquare_inf ic). apply: cleA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)