Lean Mathlib Primrec: `(Primrec.const n).add` fails; use Primrec.nat_add.comp

In current Mathlib, writing (Primrec.const n).add hf gives 'Invalid field notation: Function Nat.Primrec.add does not have a usable parameter', because dot notation on Primrec resolves into the Nat.Primrec namespace, and the error then cascades into whnf timeouts on the enclosing declaration. Write Primrec.nat_add.comp (Primrec.const n) hf instead. A related gotcha: after simp [step, show P from h] unfolds a classical dite whose branch uses h.choose, the goal can be left as h'.choose = h.choose ∧ ... with two different proofs of the same Prop. exact ⟨rfl, rfl⟩ closes it by proof irrelevance.