Mathlib.Init.Data.Nat.Basic
source
A computable version of Nat.rec. Workaround until Lean has native support for this.
Nat.rec