proposition: Fact ra_plus_val n m : ⟦ra_plus⟧ (n##m##vec_nil) (n+m).
proof: Proof. apply ra_plus_rel; 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)