Further lemmas about the integers #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. The distinction between this file and
data.int.order.basicis not particularly clear. They are separated by now to minimize the porting requirements for tactics during the transition to mathlib4. After
data.rat.orderhas been ported, please feel free to reorganize these two files.