abel
G : Type u_1
inst✝ : OrderedAddCommGroup G
f : AlmostHom G
bound' : ℕ
hₐ : ∀ (g : G), |toFun f (-g) - -toFun f g| ≤ bound'
bound : ℤ
h : ∀ {g : G}, g ≥ 0 → toFun f g ≥ bound
g : G
h_g : g ∈ Set.Iic 0
⊢ toFun f g - -toFun f (-g) = toFun f (-g) - -toFun f g
no goals