## Stream: Is there code for X?

### Topic: nat.rec_succ

#### Eric Wieser (Sep 10 2020 at 14:05):

Is this builtin to mathlib or lean somewhere?

lemma rec_succ {C: ℕ → Type} {zero_f : C 0} {succ_f : Π n, C n → C n.succ} {n : ℕ} :
@nat.rec C zero_f succ_f (n + 1) = succ_f n (@nat.rec C zero_f succ_f n) := rfl


In general, it seems like if I have an inductive rec operating on a object of a known constuctor, I should be able to unfold it one level.

#### Eric Wieser (Sep 10 2020 at 14:06):

( I needed this for a proof about a deliberately awkward def in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/recursive.20let.20in/near/209644962)

#### Reid Barton (Sep 10 2020 at 14:11):

This is the L rule for some Greek letter L

#### Reid Barton (Sep 10 2020 at 14:12):

dsimp should apply it for example

#### Eric Wieser (Sep 10 2020 at 14:21):

Ahh, there's a hidden nat.add_one that I also needed

Last updated: May 07 2021 at 21:10 UTC