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

State before:
x : ENat
⊢ x ≤ ∞
Tactic:
intro n
State after:
x : ENat
n : Nat
⊢ x.leNat n = true ∨ ∞.leNat n = false

State before:
x : ENat
n : Nat
⊢ x.leNat n = true ∨ ∞.leNat n = false
Tactic:
right
State after:
case h
x : ENat
n : Nat
⊢ ∞.leNat n = false

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