proposition: Lemma ex_filterdiff_scal_fct x (f : U -> K) (g : U -> V) : (forall (n m : K), mult n m = mult m n) -> ex_filterdiff f (locally x) -> ex_filterdiff g (locally x) -> ex_filterdiff (fun t => scal (f t) (g t)) (locally x).
proof: Proof. intros Hcomm [lf Df] [lg Dg]. eexists. apply (filterdiff_scal_fct x) ; eassumption. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv