linear order on Int

Stream: mathlib4

[Yakov Pechersky]

In lean3, src#int.linear_order is in init.data.int.order. Much of that file is already in std4. Where should something like Preorder/PartialOrder/LinearOrder Int go now? Do we port the rest of that init file that std4 doesn't cover?

[Scott Morrison]

Yes.

[Kevin Buzzard]

I ported some core lean 3 bool stuff that didn't make the cut for lean 4, and I put it in Mathlib.Init.