proposition: Lemma prod_filtermap_le {T1 T2 U1 U2 F G} {FF : Filter F} {FG : Filter G} (f1 : T1 -> U1) (f2 : T2 -> U2) : filter_le (filter_prod (filtermap f1 F) (filtermap f2 G)) (filtermap (fun x => (f1 (fst x), f2 (snd x))) (filter_prod F G)).
proof: Proof. intros P [Q1 Q2 H1 H2 H]. unfold filtermap. split with (fun y => exists x, Q1 x /\ f1 x = y) (fun y => exists x, Q2 x /\ f2 x = y). - apply: filter_imp H1. intros x Qx. now exists x. - apply: filter_imp H2. intros x Qx. now exists x. intros y1 y2 [x1 [Qx1 <-]] [x2 [Qx2 <-]]. now apply H. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub