proposition: Fact Zp_invert_involutive x : inv (inv x) = x.
proof: Proof. destruct (Zp_eq_dec x Zp) as [ Hx | Hx ]; subst. + do 2 rewrite Zp_invert_spec1; auto. + apply Zp_invert_eq_not_zero. * intros H. apply Zp_invert_spec2 in Hx. rewrite H, Zp_mult_zero in Hx. apply Zp_zero_is_one in Hx; lia. * rewrite Zp_mul_comm; apply 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)