example (a b c : α) (w : c < b) (h : b ≤ a) : a - b < a - c

Stream: Is there code for X?

[Scott Morrison]

Is there I type class that I can put on α so:

example (a b c : α) (w : c < b) (h : b ≤ a) : a - b < a - c := sorry

is true?

And that has instances for both ℕ and ℤ?

[Heather Macbeth]

Maybe docs#ExistsAddOfLE (cc @Peter Nelson)?

[Yury G. Kudryashov]

Do we have an OrderedSub instance for an OrderedAddCommGroup?

[Yaël Dillies]

Yes we do. I added it a while back

[Yaël Dillies]

The lemma you want to use is docs#tsub_lt_tsub_left_of_le

[Yaël Dillies]

You can use the hypotheses from the lemma directly, or if you need something stronger (because you need another lemma) I can point you to the right mix of assumptions.

[Scott Morrison]

Thanks, @Yaël Dillies, that was what I was after, along with the product instances for OrderedSub that I've added in #5890.