proposition: Lemma Rmax_Cmod : forall x, Rmax (Rabs (fst x)) (Rabs (snd x)) <= Cmod x.
proof: Proof. case => x y /=. rewrite -!sqrt_Rsqr_abs. apply Rmax_case ; apply sqrt_le_1_alt, Rminus_le_0 ; rewrite /Rsqr /= ; ring_simplify ; by apply pow2_ge_0. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy