proposition: Lemma ex_filterdiff_scal_l : forall {F} {FF : Filter F} (x : V), ex_filterdiff (fun k : K => scal k x) F.
proof: Proof. eexists. by apply (filterdiff_scal_l x). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv