theorem C03S04.aux {x : ℝ} {y : ℝ} (h : x ^ 2 + y ^ 2 = 0) : x = 0

theorem C03S04.not_monotone_iff {f : ℝ → ℝ} : ¬Monotone f ↔ ∃ (x : ℝ) (y : ℝ), x ≤ y ∧ f x > f y