Theorem: skip_lt (Saturn/Skip.lean)

State before:
k j : Nat
c : j < k
eqn : skip k j = j := skip_below_eq c
⊢ skip k j < j + 2
Tactic:
rw [eqn]
State after:
k j : Nat
c : j < k
eqn : skip k j = j := skip_below_eq c
⊢ j < j + 2

State before:
k j : Nat
c : j < k
eqn : skip k j = j := skip_below_eq c
⊢ j < j + 2
Tactic:
apply Nat.le_step
State after:
case h
k j : Nat
c : j < k
eqn : skip k j = j := skip_below_eq c
⊢ succ j ≤ j + 1

State before:
case h
k j : Nat
c : j < k
eqn : skip k j = j := skip_below_eq c
⊢ succ j ≤ j + 1
Tactic:
apply Nat.le_refl
State after:
no goals

State before:
k j : Nat
c : ¬j < k
eqn : skip k j = j + 1 := skip_not_below_eq k j c
⊢ skip k j < j + 2
Tactic:
rw [eqn]
State after:
k j : Nat
c : ¬j < k
eqn : skip k j = j + 1 := skip_not_below_eq k j c
⊢ j + 1 < j + 2

State before:
k j : Nat
c : ¬j < k
eqn : skip k j = j + 1 := skip_not_below_eq k j c
⊢ j + 1 < j + 2
Tactic:
apply Nat.le_refl
State after:
no goals