proposition: Lemma is_lub_Rbar_eqset (E1 E2 : R -> Prop) (l : Rbar) : (forall x : R, E2 x <-> E1 x) -> is_lub_Rbar E1 l -> is_lub_Rbar E2 l.
proof: Proof. move => H [ub1 lub1] ; split. apply (is_ub_Rbar_subset E1) ; [apply H | apply ub1]. move => b Hb ; apply: lub1 ; apply (is_ub_Rbar_subset E2) ; [apply H | apply Hb]. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov