proposition: Lemma csup_s2 A z: cardinal_set A -> cardinalp z -> (forall y, inc y A -> y <c z) -> csup_s A <=c z.
proof: Proof. move => csa cz h2; apply: card_ub_sup => //. move => i /funI_P [t /h2 tA ->]; apply /cnext_pr5P => //; exact: (proj31_1 tA). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)