proposition: Lemma filterdiff_scal_l : forall {F} {FF : Filter F} (x : V), filterdiff (fun k : K => scal k x) F (fun k => scal k x).
proof: Proof. move => F FF x. apply filterdiff_linear. by apply is_linear_scal_l. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv