proposition: Lemma is_filter_lim_filter_le : forall {F G} (x : T), filter_le G F -> is_filter_lim F x -> is_filter_lim G x.
proof: Proof. intros F G x L Fx P HP. apply L. now apply Fx. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub