proposition: Lemma filterlim_fst : forall {T U F G} {FG : Filter G}, filterlim (@fst T U) (filter_prod F G) F.
proof: Proof. intros T U F G FG P HP. exists P (fun _ => True) ; try easy. apply filter_true. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub