proposition: Fact ra_prim_max_prim_rec : prim_rec ra_prim_max.
proof: Proof. Proof using Haf. apply ra_prim_min_prim_rec; auto. 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)