proposition: Lemma Rbar_locally'_le_finite : forall x : R, filter_le (Rbar_locally' x) (locally x).
proof: Proof. intros x P [eps HP] ; exists eps ; intros ; now apply HP. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub