proposition: Fact Zp_prime_integral x y : prime p -> x ⊗ y = Zp -> x = Zp \/ y = Zp.
proof: Proof. intros H1 H2. destruct (Zp_eq_dec x Zp) as [ | H ]; auto; right. revert H2; apply Zp_invertible_eq_zero, Zp_invertible_prime; 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)