proposition: Lemma filterlim_scal_l (k : K) (x : V) : filterlim (fun z => scal z x) (locally k) (locally (scal k x)).
proof: Proof. eapply filterlim_comp_2. by apply filterlim_id. by apply filterlim_const. by apply filterlim_scal. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub