linarith nnreal

Stream: general

[Johan Commelin]

Should this be in scope for linarith?

import data.real.nnreal

example (a b c d : nnreal)
  (hba : b ≤ a)
  (hcb : c ≤ b)
  (hd0 : 0 < d)
  (hdc : d ≤ c)
  (h1 : a + b + c + d = 1) :
  a + 2 * b + 3 * c + 4 * d ≤ a + 3 * b + 3 * c + 3 * d :=
begin
  linarith
end

[Johan Commelin]

Changing nnreal to real makes linarith solve it

[Johan Commelin]

linarith only looks at typeclasses, right?

[Johan Commelin]

There is a linear_ordered_semiring instance for nnreal. But maybe linarith doesn't like the semi?

[Rob Lewis]

linarith wants to subtract.