proposition: Fact Zp_opp_inj x y : ∸ x = ∸ y -> x = y.
proof: Proof. intros H; rewrite <- (Zp_opp_inv x), H; ring. 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)