proposition: Lemma miller_rabin_step' (p a r d : Z) : prime p -> 0 <= d -> 1 <= r -> a ^ (2 ^ r * d) ≡ 1 [p] -> a ^ (2 ^ (r - 1) * d) ≡ 1 [p] \/ a ^ (2 ^ (r - 1) * d) ≡ - 1 [p].
proof: Proof. intros pp d0 r1 e. apply miller_rabin_step; auto; try lia. exact_eq e. do 4 f_equal. lia. Qed.
imports: Coq(ZArith Znumtheory Lia Psatz List Bool) Coqtail(Ztools Zeqm Zlittle_fermat Zpow Zprime)