Theorem: Nat.sub_self_sub_eq_min (One.lean)

State before:
n k : ℕ
⊢ n - (n - k) = Nat.min n k
Tactic:
conv => left; right; rw [Nat.sub_eq_sub_min]
State after:
n k : ℕ
⊢ n - (n - min n k) = Nat.min n k

State before:
n k : ℕ
⊢ n - (n - min n k) = Nat.min n k
Tactic:
rw [Nat.sub_sub_self]
State after:
n k : ℕ
⊢ min n k ≤ n

State before:
n k : ℕ
⊢ min n k ≤ n
Tactic:
simp only [min_le_iff, ge_iff_le, le_refl, true_or]
State after:
no goals