proposition: Fact ra_not_val n : ⟦ra_not⟧ (n##vec_nil) (1-n).
proof: Proof. exists (1##n##vec_nil); split; auto. pos split; simpl; 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)