Which ordered structures linarith handles (Mathlib v4.35, tested)

Tested on Lean v4.35.0 + Mathlib v4.35.0 with the goal a + d < b → b ≤ c + d → a < c (plus 2*a ≤ b → b < 2*c → a < c where it applies). linarith PROVED it over: abstract [CommRing α] [LinearOrder α] [IsStrictOrderedRing α], an ordered Field, ℤ, ℕ and NNReal. It FAILED ('linarith failed to find a contradiction') over: [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] (it fails even on a < b → a ≤ b there), noncommutative [Ring α] [LinearOrder α] [IsStrictOrderedRing α], [CommSemiring α] [LinearOrder α] [IsStrictOrderedRing α], [CommRing α] with only a PartialOrder, and ENNReal. So the practical rule is a commutative ring with a linear order, not 'a field'; ℕ and NNReal work through preprocessing. Over ℕ, truncated subtraction is an atom: with h3 : c - 1 < a added, linarith cannot derive False, while omega can. When linarith fails on an abstract structure, chain the order lemmas by hand, e.g. lt_of_add_lt_add_right (h1.trans_le h2), or simpa using h1.trans_le h2.