proposition: Lemma Rbar_lub_rw (E1 E2 : Rbar -> Prop) : (forall x, E1 x <-> E2 x) -> Rbar_lub E1 = Rbar_lub E2.
proof: Proof. intro Hs ; apply Rbar_le_antisym ; apply Rbar_lub_subset ; intros x H ; apply Hs ; auto. Qed.
imports: Coq(Reals ssreflect) Rbar Rcomplements Markov