proposition: Lemma is_derive_filterdiff_C_R (f : C -> C) (x : C) (df : C -> C) : is_linear df -> is_derive (V := C_NormedModule) f x (df 1) -> filterdiff (U := C_R_NormedModule) (V := C_R_NormedModule) f (locally x) df.
proof: Proof. move => Hdf [Lf Hf]. split => //. apply is_linear_C_R. split ; apply Hdf. intros y Hy eps. apply: locally_le_locally_norm. case: (fun Hy => locally_norm_le_locally _ _ (Hf y Hy eps)) => {Hf} /= delta Hf => //. apply locally_C, Hy. by apply locally_C, Hf. exists delta => /= z Hz. rewrite -!Cmod_norm. rewrite -{1}(Cmult_1_r (minus (G := C_R_NormedModule) z y)). rewrite linear_scal. by apply Hf. by apply Hdf. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Coquelicot)