proposition: Lemma linear_zero (l : U -> V) : is_linear l -> l zero = zero.
proof: Proof. intros Hl. rewrite -(scal_zero_l zero). rewrite linear_scal. exact (scal_zero_l (l zero)). exact Hl. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv