proposition: Fact ra_proj_val n (v : vec nat n) p : ⟦ra_proj p⟧ v (vec_pos v p).
proof: Proof. 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)