@[simp]
@[simp]
@[simp]
theorem
USize.mod_toNat
(a : USize)
(b : USize)
:
USize.toNat (a % b) = USize.toNat a % USize.toNat b
@[simp]
theorem
USize.div_toNat
(a : USize)
(b : USize)
:
USize.toNat (a / b) = USize.toNat a / USize.toNat b
@[simp]