proposition: Lemma linear_opp (l : U -> V) (x : U) : is_linear l -> l (opp x) = opp (l x).
proof: Proof. intros Hl. apply plus_reg_r with (l x). rewrite <- linear_plus. rewrite !plus_opp_l. by apply linear_zero. exact Hl. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv