add_lt_of_lt_sub

Stream: Is there code for X?

[Yaël Dillies]

Is there any typeclass between ℕ and ∀ a b c, a < b - c → a + c < b? That is, a typeclass instantiated by ℕ that implies ∀ a b c, a < b - c → a + c < b.

[Yaël Dillies]

Whoops sorry this should be in #Is there code for X?

[Notification Bot]

This topic was moved here from #general > add_lt_of_lt_sub by Johan Commelin

[Yaël Dillies]

The closest lemma is docs#add_lt_of_lt_sub_right, but that assumes a group.

[Kevin Buzzard]

If you're not assuming an add_group, where is sub coming from? What non-groups have a sub other than nat?

[Eric Wieser]

pi / finsupp / dfinsupp with nat in the codomain

[Yaël Dillies]

and all the stuff respecting has_ordered_sub

[Yaël Dillies]

I don't care where it's coming from, I only want its properties.

[Yury G. Kudryashov]

I think that has_ordered_sub + linear_order should imply a < b - c <-> a + c < b. Just try rw [← not_le, ← not_le, sub_le_iff_right].