proposition: Fact Zp_invertible_eq_zero x y : Zp_invertible x -> x ⊗ y = Zp -> y = Zp.
proof: Proof. intros (i & Hi) H1. rewrite <- (Zp_mult_one y), <- Hi at 1. rewrite <- Zp_mul_assoc, H1; 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)