linarith does not know trichotomy?

Stream: mathlib4

[Siddharth Bhat]

Consider the MWE:

import Mathlib.Tactic
theorem linarith_failure (x y : nat) (h1 : ¬ (x = y)) (h2 : ¬ (x < y)) : x > y :=
  by
    try linarith
    sorry

shouldn't linarith be able to prove this?

[Mario Carneiro]

note re: MWEs: don't suppress errors which are the point of the test. Just use linarith, not try linarith; sorry

[Mario Carneiro]

import Mathlib.Tactic
theorem linarith_failure (x y : Nat) (h1 : ¬ (x = y)) (h2 : ¬ (x < y)) : x > y := by
  linarith (config := {splitNe := true})