Should `linearith` be able to solve this?

Stream: Is there code for X?

[Jujian Zhang]

Is the following inequality true for any linearly ordered additive commutative monoid? linearith doesn't know how to solve this. linearith doesn't know how to solve this when ι is linear_ordered_ring. But linearith knows how to do linear_ordered_field case.

example {ι : Type*} [linear_ordered_add_comm_monoid ι] (a b c d : ι) (h : a + b = c + d) (h' : a < c) : (d < b) :=
begin
  linarith,
end

[Yaël Dillies]

It needs to be cancel_

[Jujian Zhang]

Of course! Thank you!

[Jujian Zhang]

Wait, linear_ordered_cancel_add_comm_monoid didn't make linearith work

[Yaël Dillies]

Hmm, that's weird, because it's really a matter of applying add_lt_add_of_le_of_lt now.

[Jujian Zhang]

linearith fails perhaps because it cannot find instance covariant_class ι ι has_add.add has_lt.lt