proposition: Fact Zp_prime_square_eq_square x y : prime p -> x⊗x = y⊗y <-> x = y \/ x = ∸y.
proof: Proof. intros H1; split. + intros H2. assert ((x⊕∸y)⊗(x⊕y) = Zp) as H3. { rewrite Zp_mult_plus_distr_l, Zp_mult_plus_distr_r, H2; ring. } apply Zp_prime_integral in H3; auto. destruct H3 as [ H3 | H3 ]; [ left | right ]; rewrite Zp_opp_plus_eq in H3; rewrite H3; ring. + intros [ | ]; subst x; 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)