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

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

State before:
x : ENat
n : Nat
⊢ x.leNat n = true ∨ x.leNat n = false
Tactic:
cases x.leNat n <;> trivial
State after:
no goals