Theorem: Imo2006P5.Int.add_eq_add_of_natAbs_eq_of_natAbs_eq (Compfiles/Imo2006P5.lean)

State before:
a b c d : ℤ
hne : a ≠ b
h₁ : (c - a).natAbs = (d - b).natAbs
h₂ : (c - b).natAbs = (d - a).natAbs
⊢ a + b = c + d
Tactic:
omega
State after:
no goals