Theorem: AlmostAdditive.neg (RealsQuasiMorphisms/Basic.lean)

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ : G → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ |-f (x + y) - -f x - -f y| = |-(-f (x + y) - -f x - -f y)|
Tactic:
rw [Int.natAbs_neg]
State after:
no goals

State before:
G : Type u_1
inst✝ : AddCommGroup G
f : G → ℤ
bound : ℕ
h : AlmostAdditive f bound
f₁ : G → ℤ
bound₁ : ℕ
h₁ : AlmostAdditive f₁ bound₁
f₂ : G → ℤ
bound₂ : ℕ
h₂ : AlmostAdditive f₂ bound₂
x y : G
⊢ -(-f (x + y) - -f x - -f y) = f (x + y) - f x - f y
Tactic:
linarith
State after:
no goals