Nat to UInt32

Stream: Is there code for X?

[Asei Inoue]

how to show this?

  theorem _root_.UInt32.ofNat_le_iff {m n : Nat} (hm : m < UInt32.size) (hn : n < UInt32.size)
    : UInt32.ofNat m ≤ UInt32.ofNat n ↔ m ≤ n := by
    sorry

[Ruben Van de Velde]

theorem _root_.UInt32.ofNat_le_iff {m n : Nat} (hm : m < UInt32.size) (hn : n < UInt32.size) :
    UInt32.ofNat m ≤ UInt32.ofNat n ↔ m ≤ n := by
  rw [UInt32.le_iff_toNat_le]
  simp only [UInt32.toNat_ofNat]
  rw [Nat.mod_eq_of_lt hm]
  rw [Nat.mod_eq_of_lt hn]

Found by searching for UInt32.ofNat, LE.le on loogle, then simp?, then rw?

[Asei Inoue]

@Ruben Van de Velde Thank you!