proposition: Lemma filterdiff_id (F : (V -> Prop) -> Prop) : filterdiff (fun y => y) F (fun y => y).
proof: Proof. apply filterdiff_linear. by apply is_linear_id. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv