proposition: Lemma csup_s1 A (x := csup_s A): cardinal_set A -> (forall y, inc y A -> y <c x).
proof: Proof. move => csa y yA. apply /(cnext_pr5P (csa _ yA)); apply: card_sup_ub. move => t /funI_P [z za ->]; exact: (CS_cnext (csa _ za)). by apply /funI_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)