proposition: Lemma ex_filterdiff_scal_r_fct : forall {F} {FF : Filter F} (k : K) (f : U -> V), (forall (n m : K), mult n m = mult m n) -> ex_filterdiff f F -> ex_filterdiff (fun x => scal k (f x)) F.
proof: Proof. move => F FF k f Hcomm [lf Df]. eexists. apply (filterdiff_scal_r_fct k) ; eassumption. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv