proposition: Fact ra_iter_prim_rec : prim_rec ra_iter.
proof: Proof. Proof using Haf. apply ra_iter_n_prim_rec; ra prim rec. 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)