cases hx : e.leNat x with
| true => rw [leNat_coe_eq_true_iff_le, ←leNat_iff_toNat_le, hx]
| false =>
rw [←Bool.not_eq_true] at hx ⊢
apply mt _ hx
intro hx
rw [leNat_iff_toNat_le _ h]
rwa [leNat_coe_eq_true_iff_le] at hx
case leNat.h
e : ENat
h : e.IsFinite
x : Nat
⊢ (ENat.ofNat (e.toNat h)).leNat x = e.leNat x
no goals