no goals
n m : ℕ
⊢ 0 ≤ ofNat n → 0 ≤ ofNat m → natAbs (ofNat n + ofNat m) = natAbs (ofNat n) + natAbs (ofNat m)
simp
no goals
x✝ : ℤ
n : ℕ
⊢ 0 ≤ x✝ → 0 ≤ -[n+1] → natAbs (x✝ + -[n+1]) = natAbs x✝ + natAbs -[n+1]
simp
no goals
n : ℕ
x✝ : ℤ
⊢ 0 ≤ -[n+1] → 0 ≤ x✝ → natAbs (-[n+1] + x✝) = natAbs -[n+1] + natAbs x✝
simp