Theorem: skip_le_succ (Saturn/Skip.lean)

State before:
n k j : Nat
⊢ j < n → skip k j < n + 1
Tactic:
intro hyp
State after:
n k j : Nat
hyp : j < n
⊢ skip k j < n + 1

State before:
n k j : Nat
hyp : j < n
⊢ skip k j < n + 1
Tactic:
apply Nat.le_trans (skip_lt k j)
State after:
n k j : Nat
hyp : j < n
⊢ j + 2 ≤ n + 1

State before:
n k j : Nat
hyp : j < n
⊢ j + 2 ≤ n + 1
Tactic:
apply Nat.succ_lt_succ
State after:
case a
n k j : Nat
hyp : j < n
⊢ j < n

State before:
case a
n k j : Nat
hyp : j < n
⊢ j < n
Tactic:
exact hyp
State after:
no goals