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