Complex.norm_le_norm_two_mul_sub_of_re_le

@[blueprint "Complex.norm_le_norm_two_mul_sub_of_re_le"  (title := "Complex.norm-le-norm-two-mul-sub-of-re-le")  (statement := /--    Let $M>0$ and let $x$ be a complex number such that    $\Re x\leq M$. Then, $|x|\leq|2M - x|$.  -/)  (proof := /--    We square both sides and simplify to obtain the equivalent    inequality $$0\leq 4M^2 -4M\Re x,$$ which follows directly    from the assumption $\Re x\leq M$ and the positivity of $M$.  -/)  (latexEnv := "lemma")]lemma Complex.norm_le_norm_two_mul_sub_of_re_le {M : ℝ}    {x : ℂ} (Mpos : 0 < M) (hyp_re_x : x.re ≤ M) :    ‖x‖ ≤ ‖2 * M - x‖ := by  rw [← sq_le_sq₀ (by positivity) (by positivity)]  repeat rw [Complex.sq_norm, Complex.normSq_apply]  rw [calc    (2 * M - x).re * (2 * M - x).re +        (2 * M - x).im * (2 * M - x).im =      (2 * M - x.re) * (2 * M - x.re) +        x.im * x.im := by simp    _ = x.re * x.re +        (x.im * x.im + 4 * M * (M - x.re)) := by ring]  bound