proposition: Lemma cpow_less_ec_pr1 x y: cardinalp y -> exists a, cpow_less_ec_prop x (cnext y) a.
proof: Proof. move=> cy. exists y; split; first by move: (cnext_pr1 cy) => [_ pb _]. move => b yb /(cnext_pr4 cy) bs; by rewrite (cleA bs yb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)