Primitive-recursive column membership and witness search

Membership in e.pairColumn and the bounded fresh-witness search Nat.leastInPairColumn e b are primitive recursive uniformly in e and b.

theorem Primrec.mem_pairColumn : PrimrecRel fun (e n : ℕ) => n ∈ e.pairColumn

Membership in e.pairColumn is primitive recursive uniformly in e and n.

theorem Primrec.nat_leastInPairColumn : Primrec₂ Nat.leastInPairColumn

Selecting the least member of e.pairColumn at or above b is primitive recursive.