proposition: Lemma Rbar_is_glb_ext (E1 E2 : Rbar -> Prop) (l : Rbar) : (forall x, E1 x <-> E2 x) -> (Rbar_is_glb E1 l) -> (Rbar_is_glb E2 l).
proof: Proof. intros Heq (H1, H2) ; split. apply (Rbar_is_lb_subset _ E1) ; auto ; intros x Hx ; apply Heq ; auto. intros b Hb ; apply H2 ; apply (Rbar_is_lb_subset _ E2) ; auto ; intros x Hx ; apply Heq ; auto. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov