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