proposition: Fact Zp_opp_invertible x : Zp_invertible x <-> Zp_invertible (∸ x).
proof: Proof. split; intros (i & Hi); exists (∸ i); rewrite <- Hi; 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)