Theorem: LoVe.min_add_add_if (LoVe/Lectures/LoVe05_FunctionalProgramming_Demo.lean)

State before:
l m n : ℕ
h : m ≤ n
⊢ min (m + l) (n + l) = min m n + l
Tactic:
simp [min, h]
State after:
no goals

State before:
l m n : ℕ
h : ¬m ≤ n
⊢ min (m + l) (n + l) = min m n + l
Tactic:
simp [min, h]
State after:
no goals