proposition: Lemma is_derive_n_scal_l (f : R -> R) (n : nat) (a x l : R) : is_derive_n f n x l -> is_derive_n (fun y => a * f y) n x (a * l).
proof: Proof. case: n x => /= [ | n] x Hf. by rewrite Hf. eapply filterdiff_ext_lin. apply filterdiff_ext with (fun y => a * Derive_n f n y). move => t ; by rewrite Derive_n_scal_l. apply @filterdiff_scal_r_fct ; try by apply locally_filter. by apply Rmult_comm. apply Hf. move => /= y. rewrite /scal /= /mult /=. ring. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv