Theorem: MyNat.add_pred (TheoremProvingLean/inductive_types.lean)

State before:
m n : Nat
⊢ n ≠ zero → m + pred n = pred (m + n)
Tactic:
intro
State after:
m n : Nat
a✝ : n ≠ zero
⊢ m + pred n = pred (m + n)

State before:
m n : Nat
a✝ : n ≠ zero
⊢ m + pred n = pred (m + n)
Tactic:
match n with
| zero => contradiction
| succ l =>
  rw [add_succ, pred_succ, pred_succ]
State after:
no goals

State before:
m n : Nat
a✝ : zero ≠ zero
⊢ m + pred zero = pred (m + zero)
Tactic:
contradiction
State after:
no goals

State before:
m n l : Nat
a✝ : succ l ≠ zero
⊢ m + pred (succ l) = pred (m + succ l)
Tactic:
rw [add_succ, pred_succ, pred_succ]
State after:
no goals