proposition: Lemma cpow_less_pr3 x y: \0c <c x -> natp y -> x ^<c (csucc y) = x ^c y.
proof: Proof. move=> [[_ cx _] xnz] yN. apply: cleA; last by apply: cpow_less_pr2; apply: cltS. apply: card_ub_sup. - fprops. - move => i /funI_P [z zi ->]; apply: cpow_Mlele; fprops. have cs: cardinalp (csucc y) by apply: CS_succ. by move: zi => /(cardinals_ltP cs) /(cltSleP yN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)