fact: Definition codeNth (n m:nat) : nat := let X := nat_rec (fun _ : nat => nat) m (fun _ Hrecn : nat => cPairPi2 (pred Hrecn)) n in cPairPi1 (pred X).
imports: Coq(Arith Lists.List Lia) hydras(extEqualNat primRec) Extraction