proposition: Lemma osup_U1 E x: ordinal_set E -> ordinalp x -> \osup (E +s1 x) = omax (\osup E) x.
proof: Proof. move => ose ox. have osu: ordinal_set (E+s1 x). by move => t /setU1_P; case; [ move/ose | move ->]. have os:= (OS_sup ose). move: (omax_p1 os ox) => [qa qb]. apply: oleA. apply: (ord_ub_sup (proj32 qb)) => t /setU1_P; case => h; last by ue. by apply: oleT qa; apply:ord_sup_ub. apply: (omax_p0); last by apply: (ord_sup_ub osu); fprops. by apply: ord_sup_M osu; apply:sub_setU1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)