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

State before:
n : Nat
x : ENat
⊢ x.leNat n = false → ENat.ofNat n < x
Tactic:
intro h
State after:
n : Nat
x : ENat
h : x.leNat n = false
⊢ ENat.ofNat n < x

State before:
n : Nat
x : ENat
h : x.leNat n = false
⊢ ENat.ofNat n < x
Tactic:
exists n
State after:
n : Nat
x : ENat
h : x.leNat n = false
⊢ (ENat.ofNat n).leNat n = true ∧ x.leNat n = false

State before:
n : Nat
x : ENat
h : x.leNat n = false
⊢ (ENat.ofNat n).leNat n = true ∧ x.leNat n = false
Tactic:
constructor
State after:
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

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

State before:
case left
n : Nat
x : ENat
h : x.leNat n = false
⊢ n ≤ n
Tactic:
exact Nat.le_refl _
State after:
no goals

State before:
case right
n : Nat
x : ENat
h : x.leNat n = false
⊢ x.leNat n = false
Tactic:
exact h
State after:
no goals