Theorem: Nat.succ_le_succ' (Fpil/Chap10/Sec04.lean)

State before:
n m : Nat
⊢ n ≤ m → succ n ≤ succ m
Tactic:
intro h
State after:
n m : Nat
h : n ≤ m
⊢ succ n ≤ succ m

State before:
n m : Nat
h : n ≤ m
⊢ succ n ≤ succ m
Tactic:
induction h with
| refl => constructor
| step _ ih =>
  constructor
  assumption
State after:
no goals

State before:
case refl
n m : Nat
⊢ succ n ≤ succ n
Tactic:
constructor
State after:
no goals

State before:
case step
n m m✝ : Nat
a✝ : Nat.le n m✝
ih : succ n ≤ succ m✝
⊢ succ n ≤ succ (succ m✝)
Tactic:
constructor
State after:
case step.a
n m m✝ : Nat
a✝ : Nat.le n m✝
ih : succ n ≤ succ m✝
⊢ Nat.le (succ n) (m✝ + 1)

State before:
case step.a
n m m✝ : Nat
a✝ : Nat.le n m✝
ih : succ n ≤ succ m✝
⊢ Nat.le (succ n) (m✝ + 1)
Tactic:
assumption
State after:
no goals