Preliminary to removing the order dependency from Mathlib/Data/Nat/Defs.lean, but that needs a little more work
Mathlib/Data/Nat/Defs.lean