proposition: Lemma cnext_pr4P y: cardinalp y -> forall x, (x <c cnext y <-> x <=c y).
proof: Proof. move => cy x; split; first by apply: cnext_pr4. move => sb; exact:(cle_ltT sb (cnext_pr2 cy)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)