proposition: Lemma Cmod_2Rmax : forall x, Cmod x <= sqrt 2 * Rmax (Rabs (fst x)) (Rabs (snd x)).
proof: Proof. case => x y /= ; apply Rmax_case_strong => 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 ssreflect) Rcomplements Rbar Continuity Derive Hierarchy