proposition: Fact Zp_invertible_cancel_l x y z : Zp_invertible x -> x⊗y = x⊗z -> y = z.
proof: Proof. intros (i & Hi) H. rewrite <- (Zp_mult_one y), <- Hi, <- Zp_mul_assoc, H, Zp_mul_assoc, Hi, 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)