proposition: Lemma ex_filterdiff_minus_fct {F} {FF : Filter F} (f g : U -> V) : ex_filterdiff f F -> ex_filterdiff g F -> ex_filterdiff (fun u => minus (f u) (g u)) F.
proof: Proof. intros [lf Df] [lg Dg]. eexists. apply filterdiff_minus_fct ; eassumption. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv