proposition: Lemma BR_sup_exists X: sub X BR -> nonempty X -> bounded_above BR_order X -> has_supremum BR_order X.
proof: Proof. move => pa pb pc. have [or sr] :=BR_osr. move: (pb) => [x0 x0X]. move:(pa _ x0X) => /BR_P [ra rb rc rd re]. have Xsr: sub X (substrate BR_order) by rewrite sr. move: pc => [z []]; rewrite /upper_bound sr => zr za. set Y := intersection X. have YQ: sub Y BQ by move => t ty; exact: (ra _ (setI_hi ty x0X)). have zY: sub z Y. move => t tx0;apply/setI_P => // i iX. by move: (za _ iX) => /BR_gleP [_ _]; apply. have neY: nonempty Y. by move /BR_P: zr => [_ [t tz] _ _ _]; exists t; apply:zY. have neQ: Y <> BQ. move => h; move: (setC_ne (conj ra rc)) => [t /setC_P [ta tb]]. by move: ta; rewrite - h => ty; move: (setI_hi ty x0X). have Yr:forall x y, inc x Y -> x <q y -> inc y Y. move => x y xY h; apply/(setI_P pb) => i iX. move:(pa _ iX) => /BR_P [_ _ _ ra' _]; apply:(ra' _ _ (setI_hi xY iX) h). case: (p_or_not_p (exists2 w, inc w BQ & Y = Zo BQ (fun z => w <=q z))). move => [w wq Yv]. set Y':= BR_of_Q w. have H: realp Y' by apply:RS_of_Q. have Ha: sub Y' Y by rewrite Yv => t /Zo_P [tq [ta _]]; apply:Zo_i. exists Y'; apply/(lubP or Xsr); rewrite /upper_bound sr; split => //. split => // y yX; apply/BR_gleP; split => //; first by apply:pa. move => t /Ha ty; exact:(setI_hi ty yX). move => Z [Za Zb];apply/BR_gleP; split => // t tz. have: inc t Y. by apply/(setI_P pb) => i iX; move:(Zb _ iX) => /BR_gleP [_ _]; apply. case: (equal_or_not w t) => ea; last first. by rewrite Yv => /Zo_P [ta tb]; apply:Zo_i. move /BR_P: Za => [_ _ _ _ ha]; move:(ha _ tz) => [w']; rewrite - ea. move => sa sb sc. have: inc w' Y. by apply /(setI_P pb) => i iX; move:(Zb _ iX) => /BR_gleP [_ _]; apply. rewrite Yv; move/Zo_hi => sd; BQo_tac. move => Ha. have ub: forall x, inc x Y -> exists2 y, inc y Y & y <q x. move => a aY;move: (YQ _ aY) => aQ; ex_middle bad. have h: forall y, inc y Y -> a <=q y. move => y yY; case:(qleT_el aQ (YQ _ yY)) => // ya; case bad; ex_tac. case: Ha; exists a => //; set_extens t. move/h => aq; apply/Zo_P; split => //; rewrite -/(ratp _); BQo_tac. move => /Zo_P [tq aq]; case: (equal_or_not a t) => eq; first by ue. apply: (Yr _ _ aY (conj aq eq)). have H: realp Y by apply/BR_P. exists Y; apply/(lubP or Xsr); rewrite /upper_bound sr; split => //. split => // y yX; apply/BR_gleP; split => //; first by apply:pa. move => t ty; exact:(setI_hi ty yX). move => Z [Za Zb];apply/BR_gleP; split => // t tz; apply/(setI_P pb). by move => i iX; move:(Zb _ iX) => /BR_gleP [_ _]; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)