Theorem: C03S05.MyAbs.abs_add (LeanInRome/S3_Logic/S05_Disjunction.lean)

State before:
x✝ y✝ x y : ℝ
⊢ |x + y| ≤ |x| + |y|
Tactic:
sorry
State after:
no goals