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