linarith nat

Stream: general

[Patrick Massot]

Is it part of the known limitations of linarith that I can't do better than

example  (n m : ℕ) (h : 0 < n) (h' : ¬ m < n) : m - n < m :=
begin
  apply nat.sub_lt ;
  linarith
end

I would like to get rid of the first line?

[Patrick Massot]

@Rob Lewis

[Rob Lewis]

To linarith, m - n is some arbitrary constant with type nat that it knows no extra information about. So no, it shouldn't be expected to solve that.