English
The second projection from a product is primitive recursive: Prod.snd.
Русский
Вторая проекция из произведения примрrec: Prod.snd.
LaTeX
$$$$ \\mathrm{Primrec}(\\mathrm{Prod.snd}) $$$$
Lean4
theorem snd {α β} [Primcodable α] [Primcodable β] : Primrec (@Prod.snd α β) :=
((casesOn' zero
((casesOn' zero (Nat.Primrec.succ.comp right)).comp (pair right ((Primcodable.prim β).comp left)))).comp
(pair right ((Primcodable.prim α).comp left))).of_eq
fun n => by
simp only [Nat.unpaired, Nat.unpair_pair, decode_prod_val]
cases @decode α _ n.unpair.1 <;> simp
cases @decode β _ n.unpair.2 <;> simp