proposition: Lemma is_linear_plus : is_linear (fun x : V * V => plus (fst x) (snd x)).
proof: Proof. repeat split. - move => x y. rewrite -!plus_assoc ; apply f_equal. rewrite plus_comm -!plus_assoc. by apply f_equal, @plus_comm. - move => k x. now rewrite scal_distr_l. - exists 2 ; split. exact Rlt_0_2. move => x /= ; eapply Rle_trans. by apply @norm_triangle. rewrite Rmult_plus_distr_r Rmult_1_l ; apply Rplus_le_compat. apply Rle_trans with (2 := proj1 (sqrt_plus_sqr _ _)). rewrite -> Rabs_pos_eq by apply norm_ge_0. by apply Rmax_l. apply Rle_trans with (2 := proj1 (sqrt_plus_sqr _ _)). rewrite -> (Rabs_pos_eq (norm (snd x))) by apply norm_ge_0. by apply Rmax_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv