proposition: Lemma filterdiff_minus (F : (V * V -> Prop) -> Prop) : filterdiff (fun u => minus (fst u) (snd u)) F (fun u => minus (fst u) (snd u)).
proof: Proof. apply filterdiff_linear. apply (is_linear_comp (fun u => (fst u, opp (snd u))) (fun u => plus (fst u) (snd u))). apply is_linear_prod. by apply is_linear_fst. apply is_linear_comp. by apply is_linear_snd. by apply is_linear_opp. by apply is_linear_plus. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv