proposition: Lemma ex_filterdiff_const {F} {FF : Filter F} (a : V) : ex_filterdiff (fun _ => a) F.
proof: Proof. intros. exists (fun _ => zero). by apply filterdiff_const. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv