proposition: Lemma filterdiff_const {F} {FF : Filter F} (a : V) : filterdiff (fun _ => a) F (fun _ => zero).
proof: Proof. split. by apply is_linear_zero. move => x Hx eps. apply filter_forall => y. rewrite minus_eq_zero minus_zero_r norm_zero. apply Rmult_le_pos. by apply Rlt_le, eps. by apply norm_ge_0. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv