proposition: Fact ra_cst_n_val n x v : ⟦ra_cst_n n x⟧ v x.
proof: Proof. exists vec_nil; split; auto. pos split. 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)