ink

@[simp]

theorem Fin.ofNat'_zero_val : ∀ {a : Nat} {h : a > 0}, (Fin.ofNat' 0 h).val = 0

ink

@[simp]

theorem Fin.mod_val {n : Nat} (a : Fin n) (b : Fin n) : (a % b).val = a.val % b.val

ink

@[simp]

theorem Fin.div_val {n : Nat} (a : Fin n) (b : Fin n) : (a / b).val = a.val / b.val

ink

@[simp]

theorem Fin.modn_val {n : Nat} (a : Fin n) (b : Nat) : (Fin.modn a b).val = a.val % b

ink

@[simp]

theorem USize.lt_def {a : USize} {b : USize} : a < b ↔ USize.toNat a < USize.toNat b

ink

@[simp]

theorem USize.le_def {a : USize} {b : USize} : a ≤ b ↔ USize.toNat a ≤ USize.toNat b

ink

@[simp]

theorem USize.zero_toNat : USize.toNat 0 = 0

ink

@[simp]

theorem USize.mod_toNat (a : USize) (b : USize) : USize.toNat (a % b) = USize.toNat a % USize.toNat b

ink

@[simp]

theorem USize.div_toNat (a : USize) (b : USize) : USize.toNat (a / b) = USize.toNat a / USize.toNat b

ink

@[simp]

theorem USize.modn_toNat (a : USize) (b : Nat) : USize.toNat (USize.modn a b) = USize.toNat a % b

ink

theorem USize.mod_lt (a : USize) (b : USize) (h : 0 < b) : a % b < b

ink

theorem USize.toNat.inj {a : USize} {b : USize} : USize.toNat a = USize.toNat b → a = b