Theorem: skip_no_fixedpoints (Saturn/Skip.lean)

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

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

State before:
k j : Nat
c : j < k
eqn : skip k j = j := skip_below_eq c
hyp : skip k j = k
⊢ 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
hyp : skip k j = k
⊢ j + 1 = k
Tactic:
rw [←hyp]
State after:
k j : Nat
c : ¬j < k
eqn : skip k j = j + 1 := skip_not_below_eq k j c
hyp : skip k j = k
⊢ j + 1 = skip k j

State before:
k j : Nat
c : ¬j < k
eqn : skip k j = j + 1 := skip_not_below_eq k j c
hyp : skip k j = k
⊢ j + 1 = skip k j
Tactic:
rw [eqn]
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
hyp : skip k j = k
lemEq : j + 1 = k :=
  Eq.mpr (id (congrArg (fun _a => j + 1 = _a) (Eq.symm hyp)))
    (Eq.mpr (id (congrArg (fun _a => j + 1 = _a) eqn)) (Eq.refl (j + 1)))
⊢ j < k
Tactic:
rw [←lemEq]
State after:
k j : Nat
c : ¬j < k
eqn : skip k j = j + 1 := skip_not_below_eq k j c
hyp : skip k j = k
lemEq : j + 1 = k :=
  Eq.mpr (id (congrArg (fun _a => j + 1 = _a) (Eq.symm hyp)))
    (Eq.mpr (id (congrArg (fun _a => j + 1 = _a) eqn)) (Eq.refl (j + 1)))
⊢ j < j + 1

State before:
k j : Nat
c : ¬j < k
eqn : skip k j = j + 1 := skip_not_below_eq k j c
hyp : skip k j = k
lemEq : j + 1 = k :=
  Eq.mpr (id (congrArg (fun _a => j + 1 = _a) (Eq.symm hyp)))
    (Eq.mpr (id (congrArg (fun _a => j + 1 = _a) eqn)) (Eq.refl (j + 1)))
⊢ j < j + 1
Tactic:
apply Nat.lt_succ_self
State after:
no goals