proposition: Lemma ex_filterdiff_scal : forall {F} {FF : ProperFilter F} (x : K * V), is_filter_lim F x -> (forall (n m : K), mult n m = mult m n) -> ex_filterdiff (fun t : K * V => scal (fst t) (snd t)) F.
proof: Proof. eexists. by apply (filterdiff_scal x). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv