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

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

State before:
x : ENat
n : Nat
⊢ leNat 0 n = true ∨ x.leNat n = false
Tactic:
simp only [OfNat.ofNat, leNat_coe_eq_true_iff_le]
State after:
x : ENat
n : Nat
⊢ 0 ≤ n ∨ x.leNat n = false

State before:
x : ENat
n : Nat
⊢ 0 ≤ n ∨ x.leNat n = false
Tactic:
left
State after:
case h
x : ENat
n : Nat
⊢ 0 ≤ n

State before:
case h
x : ENat
n : Nat
⊢ 0 ≤ n
Tactic:
exact Nat.zero_le ..
State after:
no goals