Commit 2022-11-01 22:54 243f55c8

chore(init/data/int): move lemmas (#525) The file Init.Data.Int.Basic contained three declarations:

• Int.LinearOrder
• Int.coe_nat_le
• Int.coe_nat_lt In mathlib3 all three of these were in other files: the first in Init.Data.Int.Order and the two last in Data.Int.Basic. I propose moving them to the corresponding mathlib4 files so that people know where to look for them. Zulip