proposition: Lemma ex_filterdiff_linear {F} (l : U -> V) : is_linear l -> ex_filterdiff l F.
proof: Proof. intro Hl ; exists l; by apply filterdiff_linear. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv