if h : m ≤ n then
  rw [Nat.min_eq_left h, Nat.min_eq_left (Nat.succ_le_succ h)]
else
  have : m ≥ n := Nat.le_of_lt (Nat.gt_of_not_le h)
  rw [Nat.min_eq_right' this, Nat.min_eq_right' (Nat.succ_le_succ this)]
m n : Nat
⊢ min (succ m) (succ n) = succ (min m n)
no goals