proposition: Lemma sqrt_plus_sqr : forall x y : R, Rmax (Rabs x) (Rabs y) <= sqrt (x ^ 2 + y ^ 2) <= sqrt 2 * Rmax (Rabs x) (Rabs y).
proof: Proof. intros x y. split. - rewrite -!sqrt_Rsqr_abs. apply Rmax_case ; apply sqrt_le_1_alt, Rminus_le_0 ; rewrite /Rsqr /= ; ring_simplify ; by apply pow2_ge_0. - apply Rmax_case_strong ; intros H0 ; rewrite -!sqrt_Rsqr_abs ; rewrite -?sqrt_mult ; try (by apply Rle_0_sqr) ; try (by apply Rlt_le, Rlt_0_2) ; apply sqrt_le_1_alt ; simpl ; [ rewrite Rplus_comm | ] ; rewrite /Rsqr ; apply Rle_minus_r ; ring_simplify ; apply Rsqr_le_abs_1 in H0 ; by rewrite /pow !Rmult_1_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub