left
case inr
x y : ENat
n₀ : Nat
hx : x.leNat n₀ = true
hy : y.leNat n₀ = false
n : Nat
h : n₀ ≤ n
⊢ x.leNat n = true ∨ y.leNat n = false
case inr.h
x y : ENat
n₀ : Nat
hx : x.leNat n₀ = true
hy : y.leNat n₀ = false
n : Nat
h : n₀ ≤ n
⊢ x.leNat n = true