proposition: Lemma filterlim_mult {K : AbsRing} (x y : K) : filterlim (fun z => mult (fst z) (snd z)) (filter_prod (locally x) (locally y)) (locally (mult x y)).
proof: Proof. by apply @filterlim_scal. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub