proposition: Fact Zp_invert_spec2 x : x <> Zp -> Zp_invert x ⊗ x = Op.
proof: Proof. apply (proj2_sig (Zp_invert_full x)). 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)