proposition: Lemma linear_minus (l : U -> V) (x y : U) : is_linear l -> l (minus x y) = minus (l x) (l y).
proof: Proof. intros Hl. rewrite /minus linear_plus // linear_opp //. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv