proposition: Fact Zp_invert_one : inv Op = Op.
proof: Proof. rewrite Zp_invert_eq_not_zero; auto. rewrite Zp_mult_one; 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)