linarith? fails while linarith finds the proofs

## Minimal reproducers

Plain `linarith` proves both of these; `linarith?` fails with
`linarith failed to find a contradiction`:

```lean
import Mathlib.Tactic.Linarith

example (x y u v : ℚ) (hu : u < v) (hv : v < u) : x < y := by linarith?  -- fails
example (a u v : ℚ) (gu : u < v) (h : a < 0) : a ≤ 0 := by linarith?     -- fails
```

