Comparing UInt64 and Nat

Stream: Is there code for X?

[Tage Johansson]

Hello,
I have the following goal:

skip : UInt64
skipped : Nat
skipped_le_skip : skipped ≤ UInt64.toNat skip
⊢ Nat.toUInt64 skipped ≤ skip

I would apreciate any help of how to solve that goal in Lean 4. Preferably without mathlib4 but using mathlib is ok if necessary.

Thanks,
Tage

[Jason Rute]

(deleted)

[Eric Wieser]

The proof should follow from the fact that UInt64.toNat is strictly monotone