rw [
  UInt.toNat_sub,
  ←Nat.add_sub_assoc (Nat.le_of_lt $ UInt.toNat_lt b),
  Nat.sub_add_comm hgt,
  Nat.add_mod_right,
  Nat.mod_eq_of_lt (trans (Nat.sub_le ..) (UInt.toNat_lt a))
]
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
hgt : toNat a ≥ toNat b
⊢ toNat (a - b) = toNat a - toNat b
no goals