proposition: Lemma cnext_pred_more E (c:= \csup (Zo E cardinalp)): (exists2 C, infinite_c C & E = cnext C) -> infinite_c c /\ E = cnext c.
proof: Proof. move => [C pa pb]. by move:(cnext_pred (proj1 pa)); rewrite - pb -/c => <-. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)