proposition: Lemma is_derive_scal_l : forall (f : K -> K) (x l : K) (k : V), is_derive f x l -> is_derive (fun x => scal (f x) k) x (scal l k).
proof: Proof. intros f x l k Df. eapply filterdiff_ext_lin. apply @filterdiff_scal_l_fct ; try by apply locally_filter. exact Df. simpl => y. apply sym_eq, scal_assoc. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv