proposition: Lemma prod_norm_triangle : forall x y : U * V, prod_norm (plus x y) <= prod_norm x + prod_norm y.
proof: Proof. intros [xu xv] [yu yv]. rewrite /prod_norm /= !Rmult_1_r. apply Rle_trans with (sqrt (Rsqr (norm xu + norm yu) + Rsqr (norm xv + norm yv))). - apply sqrt_le_1_alt. apply Rplus_le_compat. apply Rsqr_le_abs_1. rewrite -> 2!Rabs_pos_eq. apply: norm_triangle. apply Rplus_le_le_0_compat ; apply norm_ge_0. apply norm_ge_0. apply Rsqr_le_abs_1. rewrite -> 2!Rabs_pos_eq. apply: norm_triangle. apply Rplus_le_le_0_compat ; apply norm_ge_0. apply norm_ge_0. - apply Rsqr_incr_0_var. apply Rminus_le_0. unfold Rsqr ; simpl ; ring_simplify. rewrite /pow ?Rmult_1_r. rewrite ?sqrt_sqrt ; ring_simplify. replace (-2 * norm xu * norm yu - 2 * norm xv * norm yv) with (-(2 * (norm xu * norm yu + norm xv * norm yv))) by ring. rewrite Rmult_assoc -sqrt_mult. rewrite Rplus_comm. apply -> Rminus_le_0. apply Rmult_le_compat_l. apply Rlt_le, Rlt_0_2. apply Rsqr_incr_0_var. apply Rminus_le_0. rewrite /Rsqr ?sqrt_sqrt ; ring_simplify. replace (norm xu ^ 2 * norm yv ^ 2 - 2 * norm xu * norm xv * norm yu * norm yv + norm xv ^ 2 * norm yu ^ 2) with ((norm xu * norm yv - norm xv * norm yu) ^ 2) by ring. apply pow2_ge_0. repeat apply Rplus_le_le_0_compat ; apply Rmult_le_pos ; apply pow2_ge_0. apply sqrt_pos. apply Rplus_le_le_0_compat ; apply Rle_0_sqr. apply Rplus_le_le_0_compat ; apply Rle_0_sqr. replace (norm xu ^ 2 + 2 * norm xu * norm yu + norm yu ^ 2 + norm xv ^ 2 + 2 * norm xv * norm yv + norm yv ^ 2) with ((norm xu + norm yu) ^ 2 + (norm xv + norm yv) ^ 2) by ring. apply Rplus_le_le_0_compat ; apply pow2_ge_0. apply Rplus_le_le_0_compat ; apply pow2_ge_0. apply Rplus_le_le_0_compat ; apply pow2_ge_0. apply Rplus_le_le_0_compat ; apply sqrt_pos. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub