backporting Nat.Le

Stream: lean4

[Daniel Selsam]

We tried the Nat.Le forward port in Lean4 (see https://github.com/dselsam/binport/issues/15) but because of the special kernel support, it seems to require changing very delicate code on the C++ side related to staging. Is someone willing to backport the Lean4 version to Lean3? AFAICT it is the easy direction to change because you don't lose any definitional equalities.