rw [leNat_coe_eq_true_iff_le]
case mpr.inr
n : Nat
x : ENat
h✝ : ENat.ofNat (n + 1) ≤ x
h : x.leNat n = false
⊢ (ENat.ofNat n).leNat n = true ∧ x.leNat n = false
case mpr.inr
n : Nat
x : ENat
h✝ : ENat.ofNat (n + 1) ≤ x
h : x.leNat n = false
⊢ n ≤ n ∧ x.leNat n = false