proposition: Lemma filterdiff_opp_fct {F} {FF : Filter F} (f lf : U -> V) : filterdiff f F lf -> filterdiff (fun t => opp (f t)) F (fun t => opp (lf t)).
proof: Proof. intro Df. apply filterdiff_comp. by []. by apply filterdiff_opp. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv