Theorem: UInt.sub_of_toNat_ge_toNat (Algdata/Classes/UInt.lean)

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
⊢ toNat a ≥ toNat b → toNat (a - b) = toNat a - toNat b
Tactic:
intro hgt
State after:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
hgt : toNat a ≥ toNat b
⊢ toNat (a - b) = toNat a - toNat b

State before:
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
a b : α
hgt : toNat a ≥ toNat b
⊢ toNat (a - b) = toNat a - toNat b
Tactic:
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))
]
State after:
no goals