proposition: Lemma cpow_less_pr4 x y: \0c <c x -> infinite_c y -> x ^<c (cnext y) = x ^c y.
proof: Proof. move=> [[_ cx _] xnz] yi. have cy := proj1 yi. apply: cleA; last by (apply: cpow_less_pr2; apply:(cnext_pr2 cy)). apply: card_ub_sup. - fprops. - move => i /funI_P [z /Zo_hi zi ->]; apply: cpow_Meqle;fprops. apply: cnext_pr4 => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)