porting record

Stream: mathlib4

[Mario Carneiro]

While porting init.data.int.order, I came across a run of 391 lines of completely error free lean 4 text produced by synport, almost half the file. It's a small milestone but it is nice to see in any case. :tada: