proposition: Lemma olt_sup A x: ordinal_set A -> x <o (\osup A) -> exists2 z, inc z A & x <o z.
proof: Proof. move=> osA h. have ox:= proj31_1 h. ex_middle bad. have: (forall z, inc z A -> z <=o x). move => z zA;case:(oleT_el (osA _ zA) ox) => // xz; case: bad; ex_tac. move => pc;case: (oltNge h (ord_ub_sup ox pc)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)