Theorem: skip_gt_or_arg_below (Saturn/Skip.lean)

State before:
k j : Nat
c : ¬j < k
eqn : skip k j = j + 1 := skip_not_below_eq k j c
⊢ j + 1 ≤ skip k j
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 + 1

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