apply Nat.succ_le_of_lt
case isFalse
y : Nat
e : ENat
hy : e.leNat y = true
x : Nat
hle : x ≤ y
h✝ : ¬e.leNat x = true
⊢ x + 1 ≤ y
case isFalse.h
y : Nat
e : ENat
hy : e.leNat y = true
x : Nat
hle : x ≤ y
h✝ : ¬e.leNat x = true
⊢ x < y