x y : Nat
⊢ (if x ≤ y then succ x else succ y) = succ (if x ≤ y then x else y)
x y : Nat
⊢ min (succ x) (succ y) = succ (min x y)
simp [Nat.min_def, succ_le_succ_iff]
no goals
x y : Nat
⊢ (if x ≤ y then succ x else succ y) = succ (if x ≤ y then x else y)
split <;> rfl