Theorem: Int.natAbs_add (ECTate/Algebra/ValuedRing.lean)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℤ
⊢ natAbs (a + b) = max (natAbs a) (natAbs b) - min (natAbs a) (natAbs b)
Tactic:
sorry
State after:
no goals