proposition: Lemma cnext_pr1 c (a:= cnext c): cardinalp c -> [/\ cardinalp a, c <c a & forall c', c <c c' -> a <=c c'].
proof: Proof. move => cc. have H:= (cnextP cc). have ose: ordinal_set a by move => t /H [pa _]. have oe: ordinalp a. apply: ordinal_pr => // t /H [pa pb] s st. apply/H; split; first exact: (Os_ordinal pa st). exact:(cleT (sub_smaller (ordinal_transitive pa st)) pb). case: (cleT_el (CS_cardinal a) cc) => pa. by case /H: (ordinal_irreflexive oe). have pb: forall c', c <c c' -> sub a c'. move => c' cc'; move:(proj32_1 cc') => h2 t /H [sa sb]. by move /(ocle2P h2 sa): (cle_ltT sb cc') => /olt_i. have cp: cardinalp a. split => // z oz /card_eqP hh; rewrite hh in pa. move: (card_ord_le oz) => [_ _ s3]; exact: (sub_trans (pb _ pa) s3). rewrite -{2} (card_card cp); split => //. by move => c' cc'; split => //; [ exact:proj32_1 cc' | apply: pb]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)