proposition: Lemma filterdiff_C_R_is_derive (f : C -> C) (x : C) (df : C) : filterdiff (U := C_R_NormedModule) (V := C_R_NormedModule) f (locally x) (fun u => mult u df) -> is_derive (V := C_NormedModule) f x df.
proof: Proof. intros (Lf,Df). split. apply is_linear_scal_l. intros y Hy eps. apply: locally_le_locally_norm. case: (fun Hy => locally_norm_le_locally _ _ (Df y Hy eps)) => {Df} /= delta Df => //. apply locally_C, Hy. by apply locally_C, Df. exists delta => /= z Hz. rewrite /norm /= /abs /= !Cmod_norm. apply Df, Hz. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)