proposition: Fact Zp_invert_opp x : inv (∸x) = ∸(inv x).
proof: Proof. destruct (Zp_eq_dec x Zp) as [ Hx | Hx ]. + subst; rewrite Zp_opp_zero, Zp_invert_spec1, Zp_opp_zero; auto. + apply Zp_invert_eq_not_zero. * contradict Hx. rewrite <- (Zp_opp_inv x), Hx, Zp_opp_zero; trivial. * do 2 rewrite Zp_opp_mult, Zp_mul_comm. rewrite Zp_opp_inv, Zp_invert_spec2; 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)