let c' := Nat.gt_of_not_le c
case h
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ b < a
case h
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
c' : a > b := Nat.gt_of_not_le c
⊢ b < a