proposition: Fact ra_cst_n_prim n x : prim_rec (ra_cst_n n x).
proof: Proof. apply prim_rec_bool_spec; reflexivity. Qed.
imports: Arith List Lia Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list gcd crt sums finite pos vec) Undecidability.MuRec.Util(recalg recomp prim_min)