proposition: Fact nat_test_eq_spec a b : nat_test_eq a b = 0 <-> a = b.
proof: Proof. split. + intros H. destruct (eq_nat_dec a b) as [ | D ]; auto. apply nat_test_eq_spec1 in D; lia. + intros ->; apply nat_test_eq_spec0. 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)