proposition: Lemma cpow_less_pr5a x y: cardinalp x -> \2c <=c y -> x <=c x ^<c y.
proof: Proof. move=> cx y2. move: (cpow_less_pr2 x (clt_leT (clt_12) y2)). by rewrite cpowx1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)