proposition: Lemma miller_rabin_step (p a r d : Z) : prime p -> 0 <= d -> 0 <= r -> a ^ (2 ^ (r + 1) * d) ≡ 1 [p] -> a ^ (2 ^ r * d) ≡ 1 [p] \/ a ^ (2 ^ r * d) ≡ - 1 [p].
proof: Proof. intros pp Hd Hr H. apply square_roots_of_unity; auto. rewrite eqm_divide in *; try apply prime_not_0, pp. enough ((a ^ (2 ^ r * d)) ^ 2 = a ^ (2 ^ (r + 1) * d)) by congruence. assert (2 ^ (r + 1) * d = (2 ^ r * d) * 2) as -> by now rewrite Z.pow_add_r; lia || auto. rewrite (Z.pow_mul_r _ _ 2). easy. pose proof Z.pow_nonneg 2 r ltac:(lia). lia. lia. Qed.
imports: Coq(ZArith Znumtheory Lia Psatz List Bool) Coqtail(Ztools Zeqm Zlittle_fermat Zpow Zprime)