proposition: Fact ra_inject_prim_rec n : prim_rec (ra_inject n).
proof: Proof. induction n as [ | n IHn ]; simpl; split; auto. + pos split. + pos split; ra prim rec. intro; vec pos simpl. 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)