Nat.RecursiveIn has no lazy if-then-else; build it from two `prec`s with total base cases

To prove the join universal property (f ⊕ g ≤ᵀ h from f ≤ᵀ h and g ≤ᵀ h, where (f ⊕ g) n = if n % 2 = 0 then f (n/2) else g (n/2) for partial f, g), you need a case split that evaluates only the chosen branch. Nat.RecursiveIn.prec always evaluates the base case F a first, so putting f in the base diverges on odd inputs whenever f does. Fix: (1) build P with prec, a total base a ↦ ⟨a, 1⟩ and step g a ↦ ⟨g a, 0⟩, so that P ⟨a, 0⟩ = ⟨a,1⟩ and P ⟨a, 1⟩ = ⟨g a, 0⟩; (2) build Q with prec, the identity as base and step f c, so that Q ⟨c,0⟩ = c and Q ⟨c,1⟩ = f c; (3) take f ⊕ g = Q ∘ P ∘ (n ↦ ⟨n/2, n%2⟩). The proof closes by simp [Part.bind_some, Nat.unpair_pair] plus Part.bind_assoc and Part.bind_some_right. Gotcha: rw [Part.bind_some] fails on (Part.some a).bind F with F : ℕ →. ℕ, because PFun is not syntactically ℕ → Part ℕ. Use refine (Part.bind_some _ _).trans ?_ instead. Axioms side note: Primrec.succ and Primrec₂.natPair already report Classical.choice in current Mathlib.