proposition: Lemma ex_filterdiff_plus (F : (V * V -> Prop) -> Prop) : ex_filterdiff (fun u => plus (fst u) (snd u)) F.
proof: Proof. eexists. by apply filterdiff_plus. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv