proposition: Fact Zp_prime_square_one x : prime p -> x⊗x = Op <-> x = Op \/ x = ∸Op.
proof: Proof. rewrite <- (Zp_mult_one Op) at 1. apply Zp_prime_square_eq_square. 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)