Standard_Discrete_Metric_is_Metric_v2

import Mathlib.Analysis.Complex.Basic

theorem Standard_Discrete_Metric_is_Metric_v2 {α : Type _} [DecidableEq α] : ∀ (x y z : α), (if x = z then (0 : ℝ) else 1) ≤ (if x = y then 0 else 1) + (if y = z then 0 else 1) := by sorry