Theorem: N.add_succ (LeanTeaching/TD/TD02.lean)

State before:
S : Type
image_zero : S
image_succ : N → S → S
n✝ m✝ n m : N
⊢ n + succ m = succ (n + m)
Tactic:
rfl
State after:
no goals