proposition: Lemma filterlim_switch {U : CompleteSpace} F1 (FF1 : ProperFilter F1) F2 (FF2 : ProperFilter F2) (f : T1 -> T2 -> U) g h : filterlim f F1 (locally g) -> (forall x, filterlim (f x) F2 (locally (h x))) -> exists l : U, filterlim h F1 (locally l) /\ filterlim g F2 (locally l).
proof: Proof. move => Hfg Hfh. destruct (filterlim_switch_2 F1 FF1 F2 FF2 f g h Hfg Hfh) as [l Hhl]. exists l ; split. exact Hhl. case: FF2 => HF2 FF2. now apply (filterlim_switch_1 F1 FF1 F2 FF2 f g h l). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub