Commit 2026-03-02 23:05 aaaaf054

fix: linarith splitNe skips hypotheses without LinearOrder (#35990) When using linarith with splitNe := true, the tactic would fail with "failed to synthesize LinearOrder V" if any ≠ hypothesis existed on a type without a LinearOrder instance (like AddCommGroup). With this PR it just skips those hypotheses and processes only the ones it can actually split. Fixes #29963