theorem RealNumbers.triangle_inequality (x y : ℝ) : |x + y| ≤ |x| + |y|

Triangle inequality for the absolute value on ℝ: |x + y| ≤ |x| + |y| for all real numbers x and y.