mathlib

1f50530a - feat(data/set/intervals/image_preimage, algebra/ordered_monoid): new typeclass for interval bijection lemmas (#6629)

feat(data/set/intervals/image_preimage, algebra/ordered_monoid): new typeclass for interval bijection lemmas (#6629) This commit introduces a ``has_exists_add_of_le`` typeclass extending ``ordered_add_comm_monoid``; is the assumption needed so that additively translating an interval gives a bijection. We then prove this fact for all flavours of interval. https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Correct.20setting.20for.20positive.20shifts.20of.20intervals Co-authored-by: Peter Nelson <71660771+apnelson1@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>