linarith failure with divison

Stream: new members

[Jeremy Toh]

Is it intended behaviour for linarith to fail for the first example? Does Lean think of 1/2 as 0 or coerces it to be say a rational? We end up with [x + 1 - 1 ≤ 0, 1 / 2 + 1 - x ≤ 0] as the final list of facts, so I am thinking linarith should be able to come up with coefficients, in either case, to get a contradiction.

example (x : ℤ) (h1 : x < 1) (h2 : x > 1/2) : False := by
  try linarith
  sorry

example (x : ℤ) (h1 : x < 1) (h2 : 2*x > 1) : False := by
  linarith

[Ruben Van de Velde]

example (x : ℤ) (h1 : x < 1) (h2 : x > 1/2) : False := by
  simp at h2
  linarith
  done

[Ruben Van de Velde]

I guess linarith could have some support for Int's rounding division, but arguably that would be out of scope

[Jeremy Toh]

I see. It tries to change < into ≤ by adding one which changes the problem here, although it is not so bad since it fails. Thanks!