proposition: Lemma filterdiff_linear {F} (l : U -> V) : is_linear l -> filterdiff l F l.
proof: Proof. move => Hl ; split. by []. move => x Hx eps. apply Hx. apply filter_forall => y. rewrite -linear_minus // minus_eq_zero norm_zero. apply Rmult_le_pos. apply Rlt_le, eps. by apply norm_ge_0. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv