proposition: Lemma cnext_pr4 x y: cardinalp y -> x <c cnext y -> x <=c y.
proof: Proof. move => pa pb. case: (cleT_el (proj31_1 pb) pa) => // h. case: (cltNge pb (proj33 (cnext_pr1 pa) _ h)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)