Theorem: ENat.mono' (GMLInit/Data/Nat/Extended/Basic.lean)

State before:
e : ENat
x y : Nat
⊢ x ≤ y → e.leNat y = false → e.leNat x = false
Tactic:
intro h hy
State after:
e : ENat
x y : Nat
h : x ≤ y
hy : e.leNat y = false
⊢ e.leNat x = false

State before:
e : ENat
x y : Nat
h : x ≤ y
hy : e.leNat y = false
⊢ e.leNat x = false
Tactic:
rw [Bool.eq_false_iff] at hy ⊢
State after:
e : ENat
x y : Nat
h : x ≤ y
hy : e.leNat y ≠ true
⊢ e.leNat x ≠ true

State before:
e : ENat
x y : Nat
h : x ≤ y
hy : e.leNat y ≠ true
⊢ e.leNat x ≠ true
Tactic:
exact mt (mono h) hy
State after:
no goals