proposition: Lemma cpow_less_pr2 x y z: z <c y -> x ^c z <=c (x ^<c y).
proof: Proof. move=> lt1; apply: card_sup_ub; first by apply: cpow_less_pr0. apply /funI_P;exists z => //; apply /(cardinals_ltP (proj32_1 lt1)) => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)