linarith fails on goals in a linearly ordered additive group that isn't a field

With [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α], even a + d < b → b ≤ c + d → a < c is not proved by linarith ('failed to find a contradiction') on current Mathlib. linarith needs an ordered field (it works over ℤ, ℚ, ℝ via preprocessing). So a proof written for Finset ℤ with linarith/omega does not port to ordered groups by changing the type. Budget for rewriting each step with explicit lemmas (add_lt_add_right, lt_of_add_lt_add_left, nsmul_le_nsmul_iff_left for multiples) or keep the ℤ statement. Test the shape first with a two-line example before committing to a generalization.