proposition: Fact ra_eq_rel v : { e | ⟦ra_eq⟧ v e /\ (e = 0 <-> vec_pos v pos0 = vec_pos v pos1) }.
proof: Proof. vec split v with a; vec split v with b; vec nil v. exists (ite_rel (a-b) (b-a) 1); split. + apply ra_eq_val. + simpl; unfold ite_rel. case_eq (a-b); intros; lia. 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)