Theorem: Nat.succ_le_or_eq_zero_iff_le_pred (GMLInit/Data/Nat/Succ.lean)

State before:
case zero_left
x : Nat
⊢ 0 + 1 ≤ x ∨ 0 = 0 ↔ 0 ≤ x - 1
Tactic:
simp
State after:
no goals

State before:
case zero_right
y : Nat
⊢ y + 1 ≤ 0 ∨ y = 0 ↔ y ≤ 0 - 1
Tactic:
simp
State after:
no goals

State before:
case succ_succ
x y : Nat
a✝ : x + 1 ≤ y ∨ x = 0 ↔ x ≤ y - 1
⊢ x + 1 + 1 ≤ y + 1 ∨ x + 1 = 0 ↔ x + 1 ≤ y + 1 - 1
Tactic:
constructor
State after:
case succ_succ.mp
x y : Nat
a✝ : x + 1 ≤ y ∨ x = 0 ↔ x ≤ y - 1
⊢ x + 1 + 1 ≤ y + 1 ∨ x + 1 = 0 → x + 1 ≤ y + 1 - 1

case succ_succ.mpr
x y : Nat
a✝ : x + 1 ≤ y ∨ x = 0 ↔ x ≤ y - 1
⊢ x + 1 ≤ y + 1 - 1 → x + 1 + 1 ≤ y + 1 ∨ x + 1 = 0

State before:
case succ_succ.mp
x y : Nat
a✝ : x + 1 ≤ y ∨ x = 0 ↔ x ≤ y - 1
⊢ x + 1 + 1 ≤ y + 1 ∨ x + 1 = 0 → x + 1 ≤ y + 1 - 1
Tactic:
intro
| Or.inl h => exact Nat.le_of_succ_le_succ h
| Or.inr h => absurd h; apply Nat.succ_ne_zero
State after:
no goals

State before:
x y : Nat
a✝ : x + 1 ≤ y ∨ x = 0 ↔ x ≤ y - 1
x✝ : x + 1 + 1 ≤ y + 1 ∨ x + 1 = 0
h : x + 1 + 1 ≤ y + 1
⊢ x + 1 ≤ y + 1 - 1
Tactic:
exact Nat.le_of_succ_le_succ h
State after:
no goals

State before:
x y : Nat
a✝ : x + 1 ≤ y ∨ x = 0 ↔ x ≤ y - 1
x✝ : x + 1 + 1 ≤ y + 1 ∨ x + 1 = 0
h : x + 1 = 0
⊢ x + 1 ≤ y + 1 - 1
Tactic:
absurd h
State after:
x y : Nat
a✝ : x + 1 ≤ y ∨ x = 0 ↔ x ≤ y - 1
x✝ : x + 1 + 1 ≤ y + 1 ∨ x + 1 = 0
h : x + 1 = 0
⊢ ¬x + 1 = 0

State before:
x y : Nat
a✝ : x + 1 ≤ y ∨ x = 0 ↔ x ≤ y - 1
x✝ : x + 1 + 1 ≤ y + 1 ∨ x + 1 = 0
h : x + 1 = 0
⊢ ¬x + 1 = 0
Tactic:
apply Nat.succ_ne_zero
State after:
no goals

State before:
case succ_succ.mpr
x y : Nat
a✝ : x + 1 ≤ y ∨ x = 0 ↔ x ≤ y - 1
⊢ x + 1 ≤ y + 1 - 1 → x + 1 + 1 ≤ y + 1 ∨ x + 1 = 0
Tactic:
intro h
State after:
case succ_succ.mpr
x y : Nat
a✝ : x + 1 ≤ y ∨ x = 0 ↔ x ≤ y - 1
h : x + 1 ≤ y + 1 - 1
⊢ x + 1 + 1 ≤ y + 1 ∨ x + 1 = 0

State before:
case succ_succ.mpr
x y : Nat
a✝ : x + 1 ≤ y ∨ x = 0 ↔ x ≤ y - 1
h : x + 1 ≤ y + 1 - 1
⊢ x + 1 + 1 ≤ y + 1 ∨ x + 1 = 0
Tactic:
left
State after:
case succ_succ.mpr.h
x y : Nat
a✝ : x + 1 ≤ y ∨ x = 0 ↔ x ≤ y - 1
h : x + 1 ≤ y + 1 - 1
⊢ x + 1 + 1 ≤ y + 1

State before:
case succ_succ.mpr.h
x y : Nat
a✝ : x + 1 ≤ y ∨ x = 0 ↔ x ≤ y - 1
h : x + 1 ≤ y + 1 - 1
⊢ x + 1 + 1 ≤ y + 1
Tactic:
exact Nat.succ_le_succ h
State after:
no goals