proposition: Fact Zp_eq_dec : forall x y : Z_Zp, { x = y } + { x <> y }.
proof: Proof. intros (x & Hx) (y & Hy). destruct (eq_nat_dec x y) as [ | H ]. + left; apply Zp_inj; auto. + right; contradict H. apply f_equal with (f := @proj1_sig _ _) in H; auto. Qed.
imports: Arith Lia ZArith List Permutation Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list gcd prime binomial sums php) Undecidability.H10.ArithLibs(matrix)