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

State before:
x : ENat
⊢ ¬x < x
Tactic:
rw [ENat.not_lt]
State after:
x : ENat
⊢ x ≤ x

State before:
x : ENat
⊢ x ≤ x
Tactic:
exact le_refl _
State after:
no goals