Theorem: ENat.leNat_eq_false_of_coe_lt (GMLInit/Data/Nat/Extended/Order.lean)

State before:
n : Nat
x : ENat
⊢ ENat.ofNat n < x → x.leNat n = false
Tactic:
intro ⟨m, h, hm⟩
State after:
n : Nat
x : ENat
m : Nat
h : (ENat.ofNat n).leNat m = true
hm : x.leNat m = false
⊢ x.leNat n = false

State before:
n : Nat
x : ENat
m : Nat
h : (ENat.ofNat n).leNat m = true
hm : x.leNat m = false
⊢ x.leNat n = false
Tactic:
rw [leNat_coe_eq_true_iff_le] at h
State after:
n : Nat
x : ENat
m : Nat
h : n ≤ m
hm : x.leNat m = false
⊢ x.leNat n = false

State before:
n : Nat
x : ENat
m : Nat
h : n ≤ m
hm : x.leNat m = false
⊢ x.leNat n = false
Tactic:
exact mono' h hm
State after:
no goals