proposition: Fact Zp_mult_invertible x y : Zp_invertible x -> Zp_invertible y -> Zp_invertible (x ⊗ y).
proof: Proof. intros (u & H1) (v & H2); exists (u⊗v); rewrite <- (Zp_mult_one Op). rewrite <- H1 at 1. rewrite <- H2; 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)