proposition: Lemma filterdiff_plus_fct {F} {FF : Filter F} (f g : U -> V) (lf lg : U -> V) : filterdiff f F lf -> filterdiff g F lg -> filterdiff (fun u => plus (f u) (g u)) F (fun u => plus (lf u) (lg u)).
proof: Proof. intros Df Dg. apply filterdiff_comp_2. by []. by []. by apply filterdiff_plus. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv