proposition: Lemma filterdiff_scal_fct x (f : U -> K) (g : U -> V) lf lg : (forall (n m : K), mult n m = mult m n) -> filterdiff f (locally x) lf -> filterdiff g (locally x) lg -> filterdiff (fun t => scal (f t) (g t)) (locally x) (fun t => plus (scal (lf t) (g x)) (scal (f x) (lg t))).
proof: Proof. intros Hcomm Df Dg. apply (filterdiff_comp'_2 f g scal x lf lg (fun k v => plus (scal k (g x)) (scal (f x) v))) => //. by apply (filterdiff_scal (f x, g x)). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv