Theorem: tsub_tsub_eq_min (LeanCamCombi/Mathlib/Algebra/Order/Sub/Canonical.lean)

State before:
α : Type u_1
inst✝³ : CanonicallyLinearOrderedAddCommMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a - (a - b) = min a b
Tactic:
rw [tsub_eq_tsub_min _ b, tsub_tsub_cancel_of_le (min_le_left a _)]
State after:
no goals