proposition: Lemma ointv_sup1 a b: a <o b -> limit_ordinal b -> \osup (ordinal_interval a b) = b.
proof: Proof. by move=> ab lb; rewrite (ointv_sup ab) - [LHS] (limit_nonsucc lb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)