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