apply Nat.lt_of_le_of_ne hle
case isFalse.h
y : Nat
e : ENat
hy : e.leNat y = true
x : Nat
hle : x ≤ y
h✝ : ¬e.leNat x = true
⊢ x < 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