proposition: Fact Zp_inj : forall x y, proj1_sig x = proj1_sig y -> x = y.
proof: Proof. intros (x & H1) (y & H2); simpl; intros; subst; f_equal; apply lt_pirr. 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)