proposition: Lemma is_linear_scal_l (x : V) : is_linear (fun k : K => scal k x).
proof: Proof. split. - move => u v ; by apply @scal_distr_r. - move => u v /= ; apply sym_eq, @scal_assoc. - exists (norm x + 1) ; split. apply Rplus_le_lt_0_compat. apply norm_ge_0. exact Rlt_0_1. move => k /=. rewrite Rmult_plus_distr_r Rmult_1_l -(Rplus_0_r (norm (scal k x))). apply Rplus_le_compat. now rewrite Rmult_comm ; apply norm_scal. apply norm_ge_0. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv