constructor
n : Nat
x : ENat
h : x.leNat n = false
⊢ (ENat.ofNat n).leNat n = true ∧ x.leNat n = false
case left
n : Nat
x : ENat
h : x.leNat n = false
⊢ (ENat.ofNat n).leNat n = true

case right
n : Nat
x : ENat
h : x.leNat n = false
⊢ x.leNat n = false