proposition: Lemma filterdiff_scal_l_fct : forall {F} {FF : Filter F} (x : V) (f : U -> K) lf, filterdiff f F lf -> filterdiff (fun u => scal (f u) x) F (fun u => scal (lf u) x).
proof: Proof. move => F FF x f lf Df. apply (filterdiff_comp f (fun k => scal k x) lf (fun k => scal k x)). by []. apply filterdiff_linear. by apply is_linear_scal_l. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv