apply Int.natAbs_le' <;>
(apply Int.le_trans (by assumption)
solve| apply Int.le_max_left | apply Int.le_max_right)
case inl
G : Type u_1
inst✝ : LinearOrderedAddCommGroup G
f f₁ f₂ : AlmostHom G
h₁ : AlmostHom.NonNeg f
h₂ : AlmostHom.NonNeg (-f)
bound₁ bound₂ bound₃ : ℤ
h₃' : Function.BddAboveOnBy f.toFun (Set.Iic 0) bound₃
bound₄ : ℤ
h₄' : Function.BddAboveOnBy (-f).toFun (Set.Iic 0) bound₄
g : G
h_ge : 0 ≤ g
h₁' : toFun f g ≤ bound₁
h₂' : toFun (-f) g ≤ bound₂
⊢ ↑(|toFun f g|) ≤ max bound₁ bound₂
no goals