proposition: Lemma is_linear_zero : is_linear (fun _ => zero).
proof: Proof. repeat split. - move => _ _ ; by rewrite plus_zero_l. - move => k _ ; by rewrite scal_zero_r. - exists 1 ; split. exact Rlt_0_1. move => x ; rewrite Rmult_1_l norm_zero. apply norm_ge_0. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv