Theorem: skip_ge (Saturn/Skip.lean)

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

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

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

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