proposition: Lemma Rbar_locally'_le : forall x, filter_le (Rbar_locally' x) (Rbar_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