proposition: Lemma BR_inf_exists X: sub X BR -> nonempty X -> bounded_below BR_order X -> has_infimum BR_order X.
proof: Proof. move => pa pb pc. have [or sr]:= BR_osr. move: (pb) => [x0 x0X]. have Xsr: sub X (substrate BR_order) by rewrite sr. set Y := union X. have YQ: sub Y BQ by move => t /setU_P [u ua /pa h]; apply: (BRi_sQ h ua). have neY: nonempty Y. move:pb=> [z za]; move /BR_P: (pa _ za) => [_ [w wa] _ _ _]. by exists w; apply/setU_P; exists z. have YnQ: Y <> BQ. move: pc => [z]; rewrite /lower_bound sr; move => [zr za] eYQ. move/BR_P: zr => [zq _ h _ _]. move: (setC_ne (conj zq h)) => [t /setC_P [ta tb]]. move:ta; rewrite - eYQ => /setU_P [v va /za /BR_gleP [_ _ vb]]. by case: tb; apply: vb. have Yc: forall x y, inc x Y -> x <q y -> inc y Y. move => x y /setU_P[z za zb] lxy; apply/setU_P; exists z => //. move/BR_P: (pa _ zb) => [ _ _ _ h _]; apply: (h _ _ za lxy). have nlY:forall x, inc x Y -> exists2 y, inc y Y & y <q x. move => x /setU_P[z za zb]. move/BR_P: (pa _ zb) => [ _ _ _ _ h]; move: (h _ za) => [y ya yb]. exists y => //; apply/setU_P; ex_tac. have H: realp Y by apply/BR_P. exists Y; apply/(glbP or Xsr); rewrite /lower_bound sr; split => //. split => // y yX; apply/BR_gleP; split => //; first by apply:pa. by move => t ty; apply /setU_P; exists y. move => Z [Za Zb];apply/BR_gleP; split => // t /setU_P [v va vb]. by move: (Zb _ vb) => /BR_gleP [_ _]; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)