proposition: Lemma ointv_sup a b: a <o b -> \osup (ordinal_interval a b) = \osup b.
proof: Proof. move => ab. have [[oa ob _] _]:= ab; have laa:=(oleR oa). have aux: sub (ordinal_interval a b) b. by move=> t /(ointvP ob) [_] / oltP0 [_ _]. have osb:= Os_ordinal ob. apply: (ord_sup_1cofinal) => //; split => // u ub. have ou:= (osb _ ub). case: (oleT_ee oa ou) => aux1. exists u; last exact (oleR ou). by apply /(ointvP ob);split => //; apply /oltP0. by exists a => //; apply /(ointvP ob). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)