proposition: Fact ra_cst_val k v : ⟦ra_cst k⟧ v k.
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)