proposition: Lemma is_derive_scal : forall (f : R -> R) (x k df : R), is_derive f x df -> is_derive (fun x : R => k * f x) x (k * df).
proof: Proof. intros f x k df Df. change Rmult with (scal (V := R_NormedModule)). eapply filterdiff_ext_lin. apply filterdiff_scal_r_fct with (2 := Df). apply Rmult_comm. rewrite /scal /= /mult /= => y. ring. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv