Theorem: LoVe.Nat.succ_neq_self (LoVe/Lectures/LoVe05_FunctionalProgramming_Demo.lean)

State before:
n : ℕ
⊢ Nat.succ n ≠ n
Tactic:
induction n with
| zero       => simp
| succ n' ih => simp [ih]
State after:
no goals

State before:
case zero

⊢ Nat.succ Nat.zero ≠ Nat.zero
Tactic:
simp
State after:
no goals

State before:
case succ
n' : ℕ
ih : Nat.succ n' ≠ n'
⊢ Nat.succ (Nat.succ n') ≠ Nat.succ n'
Tactic:
simp [ih]
State after:
no goals