proposition: Lemma close_lim_fct : forall F1 F2 : ((T -> U) -> Prop) -> Prop, filter_le F1 F2 -> filter_le F2 F1 -> close (lim_fct F1) (lim_fct F2).
proof: Proof. intros F1 F2 H12 H21 eps t. apply close_lim => P. apply H12. apply H21. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub