simp [if_neg c]
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ b ≤ { max := fun x y => if x ≤ y then y else x }.1 a b
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ b ≤ a