proposition: Fact ra_project_prim_rec n p : prim_rec (@ra_project n p).
proof: Proof. induction p as [ | n p IHp ]; simpl; auto; split; auto. pos split; auto. 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 prim_min ra_utils)