Theorem: Nat.min_self_sub_left (One.lean)

State before:
n m : ℕ
⊢ min (n - m) n = n - m
Tactic:
rw [min_commutative]
State after:
n m : ℕ
⊢ min n (n - m) = n - m

State before:
n m : ℕ
⊢ min n (n - m) = n - m
Tactic:
apply Nat.min_self_sub_right
State after:
no goals