proposition: Lemma filterdiff_mult {K : AbsRing} : forall {F} {FF : ProperFilter F} (x : K * K), is_filter_lim F x -> (forall (n m : K), mult n m = mult m n) -> filterdiff (fun t : K * K => mult (fst t) (snd t)) F (fun t => plus (mult (fst t) (snd x)) (mult (fst x) (snd t))).
proof: Proof. intros. generalize (filterdiff_scal x H H0) ; by simpl. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv