Theorem: nat_succ_le_succ_iff (Katydid/Std/Lists.lean)

State before:
x y : ℕ
⊢ succ x ≤ succ y ↔ x ≤ y
Tactic:
apply Iff.intro
State after:
case mp
x y : ℕ
⊢ succ x ≤ succ y → x ≤ y

case mpr
x y : ℕ
⊢ x ≤ y → succ x ≤ succ y

State before:
x y : ℕ
⊢ succ x ≤ succ y → x ≤ y
Tactic:
case mp =>
  apply Nat.le_of_succ_le_succ
State after:
no goals

State before:
x y : ℕ
⊢ x ≤ y → succ x ≤ succ y
Tactic:
case mpr =>
  apply Nat.succ_le_succ
State after:
no goals

State before:
x y : ℕ
⊢ succ x ≤ succ y → x ≤ y
Tactic:
apply Nat.le_of_succ_le_succ
State after:
no goals

State before:
x y : ℕ
⊢ x ≤ y → succ x ≤ succ y
Tactic:
apply Nat.succ_le_succ
State after:
no goals