proposition: Lemma cnext_pred c: cardinalp c -> c = \csup (Zo (cnext c) cardinalp).
proof: Proof. move => cc. have oc:= (proj1 cc). set E := (Zo (cnext c) cardinalp). have cse: (cardinal_set E) by move => t /Zo_P []. have pa: inc c E. apply /Zo_P; split=> //; apply /(cnextP cc) => //. rewrite card_card //; split; fprops. apply:(cleA (card_sup_ub cse pa)). apply:(card_ub_sup cc). by move => x /Zo_P [ /(cnextP cc) [ox h]] /card_card <-. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)