proposition: Lemma osup_Un E F p: ordinal_set E -> sub F E -> finite_set F -> (forall x, inc x E -> x <o p) -> p = \osup E -> p = \osup (E -s F).
proof: Proof. move => ose sfe fse Ep -ea. move: F fse sfe; apply: finite_set_induction. by rewrite setC_0. move => F x Hr. case: (inc_or_not x F) => xF; first by rewrite (setU1_eq xF). move => h. have xE:= (h x (setU1_1 F x)). have /Hr: sub F E by move => t tt; exact: (h _ (setU1_r x tt)). set G := (E -s (F +s1 x)). have ->: (E -s F) = G +s1 x. set_extens t. move => /setC_P [te tf]; case: (equal_or_not t x) => tx. rewrite tx; fprops. by apply: setU1_r; apply/setC_P; split => // /setU1_P; case. case/setU1_P. move => /setC_P [tE /setU1_P h1]; apply /setC_P; split => // yf. by case: h1; left. by move ->; apply/setC_P. have osg: (ordinal_set G) by move => t /setC_P/proj1/ose. have ox: ordinalp x by apply:ose. rewrite (osup_U1 osg ox) /omax/Gmax; Ytac aux => // px. by case: (nesym (proj2(Ep _ xE))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)