cases x with
| zero => exact Nat.zero_le _
| succ x =>
  apply Nat.succ_le_of_lt
  apply Nat.not_le.1
  intro (h : _ ≤ x)
  rw [←leNat_iff_toNat_le, leNat_coe_eq_true_iff_le] at h
  apply Nat.not_lt.2 h
  exact Nat.lt_succ_self _
case h₂
x : Nat
⊢ x ≤ (ENat.ofNat x).toNat ⋯
no goals