proposition: Theorem square_roots_of_unity (x p : Z) : prime p -> x ^ 2 ≡ 1 [p] -> x ≡ 1 [p] \/ x ≡ -1 [p].
proof: Proof. intros pp. rewrite !eqm_divide. replace (x ^ 2 - 1) with ((x - 1) * (x + 1)) by lia. now intros H % prime_mult. all: apply prime_not_0, pp. Qed.
imports: Coq(ZArith Znumtheory Lia Psatz List Bool) Coqtail(Ztools Zeqm Zlittle_fermat Zpow Zprime)