proposition: Fact nat_test_eq_spec1 a b : a <> b -> nat_test_eq a b > 0.
proof: Proof. intros H. destruct (lt_eq_lt_dec a b) as [ [] | ]; try tauto; unfold nat_test_eq. + replace (a-b) with 0; simpl; lia. + replace (a-b) with (S (a-S b)); 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)