proposition: Fact ra_eq_val a b : ⟦ra_eq⟧ (a##b##vec_nil) (ite_rel (a-b) (b-a) 1).
proof: Proof. exists (a-b##b-a##1##vec_nil); split; auto. pos split; vec pos simpl. exists (b##a##vec_nil); split; auto. pos split; vec pos simpl. 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)