proposition: Fact nat_test_eq_spec0 a : nat_test_eq a a = 0.
proof: Proof. unfold nat_test_eq. replace (a-a) with 0; simpl; 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)