fix(inductive_types): fix compressed proof for succ_add

[blue-jam]

The compressed proof of succ_add requires itself. Since the proof is not completed yet, it uses succ_add from Lean's standard library.

If we use the proof for our nat defined in the "Defining the Natural Numbers" section, Lean returns an error: unknown identifier 'succ_add'.

Example:

namespace hidden

inductive nat : Type
| zero : nat
| succ : nat → nat

namespace nat

def add (m n : nat) : nat :=
nat.rec_on n m (fun n add_m_n, succ add_m_n)

instance : has_add nat := has_add.mk add

theorem add_succ (m n : nat) : m + succ n = succ (m + n) := rfl

-- This returns an error
theorem succ_add (m n : nat) : succ m + n = succ (m + n) :=
nat.rec_on n rfl (λ n ih, by simp only [succ_add, ih])

-- This successes
theorem succ_add' (m n : nat) : succ m + n = succ (m + n) :=
nat.rec_on n rfl (λ n ih, by simp only [add_succ, ih])

end nat

end hidden