Theorem: skip_above_eq (Saturn/Skip.lean)

State before:
n m : Nat
⊢ n ≤ m → skip n m = m + 1
Tactic:
intro hyp
State after:
n m : Nat
hyp : n ≤ m
⊢ skip n m = m + 1

State before:
n m : Nat
hyp : n ≤ m
⊢ skip n m = m + 1
Tactic:
rw [skip]
State after:
n m : Nat
hyp : n ≤ m
⊢ (match n, m with
    | n, m => if m < n then m else m + 1) =
    m + 1

State before:
n m : Nat
hyp : n ≤ m
⊢ (match n, m with
    | n, m => if m < n then m else m + 1) =
    m + 1
Tactic:
by_cases c: m < n
State after:
case inl
n m : Nat
hyp : n ≤ m
c : m < n
⊢ (match n, m with
    | n, m => if m < n then m else m + 1) =
    m + 1

case inr
n m : Nat
hyp : n ≤ m
c : ¬m < n
⊢ (match n, m with
    | n, m => if m < n then m else m + 1) =
    m + 1

State before:
case inl
n m : Nat
hyp : n ≤ m
c : m < n
⊢ (match n, m with
    | n, m => if m < n then m else m + 1) =
    m + 1
Tactic:
have c' : ¬(n ≤ m)  := Nat.not_le_of_gt c
State after:
case inl
n m : Nat
hyp : n ≤ m
c : m < n
c' : ¬n ≤ m
⊢ (match n, m with
    | n, m => if m < n then m else m + 1) =
    m + 1

State before:
case inl
n m : Nat
hyp : n ≤ m
c : m < n
c' : ¬n ≤ m
⊢ (match n, m with
    | n, m => if m < n then m else m + 1) =
    m + 1
Tactic:
contradiction
State after:
no goals

State before:
case inr
n m : Nat
hyp : n ≤ m
c : ¬m < n
⊢ (match n, m with
    | n, m => if m < n then m else m + 1) =
    m + 1
Tactic:
simp [c]
State after:
no goals