proposition: Fact ra_beta_prim_rec : prim_rec ra_beta.
proof: Proof. ra prim rec. Qed.
imports: Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_nat gcd crt sums) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.MuRec.Util(recalg recomp beta ra_utils ra_recomp)