proposition: Lemma clt_sup A x: cardinal_set A -> x <c \csup A -> exists2 z, inc z A & x <c z.
proof: Proof. move => p1 p2. have q1:= oset_cset p1. move: (oclt p2) => q2. move: (olt_sup q1 q2) => [z zA zlt]; ex_tac. exact (oclt3 (proj31_1 p2) (p1 _ zA) zlt). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)