Theorem: Nat.min_self_sub_right (One.lean)

State before:
n m : ℕ
⊢ min n (n - m) = n - m
Tactic:
simp only [ge_iff_le, tsub_le_iff_right, le_add_iff_nonneg_right, zero_le, min_eq_right]
State after:
no goals