proposition: Lemma prod_norm_scal : forall (l : K) (x : U * V), prod_norm (scal l x) <= abs l * prod_norm x.
proof: Proof. intros l [xu xv]. rewrite /prod_norm /= -(sqrt_Rsqr (abs l)). 2: apply abs_ge_0. rewrite !Rmult_1_r. rewrite -sqrt_mult. 2: apply Rle_0_sqr. apply sqrt_le_1_alt. rewrite Rmult_plus_distr_l. unfold Rsqr. apply Rplus_le_compat. replace (abs l * abs l * (norm xu * norm xu)) with ((abs l * norm xu) * (abs l * norm xu)) by ring. apply Rmult_le_compat. apply norm_ge_0. apply norm_ge_0. exact (norm_scal l xu). exact (norm_scal l xu). replace (abs l * abs l * (norm xv * norm xv)) with ((abs l * norm xv) * (abs l * norm xv)) by ring. apply Rmult_le_compat. apply norm_ge_0. apply norm_ge_0. exact (norm_scal l xv). exact (norm_scal l xv). apply Rplus_le_le_0_compat ; apply Rle_0_sqr. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub