proposition: Lemma mainloop_spec n a d s x : x = pow_mod n a (Z.pos d) -> mainloop n s x = existsb (fun r => pow_mod n a (2 ^ r * Z.pos d) =? n - 1) (Zseq 0 s).
proof: Proof. replace (Z.pos d) with (2 ^ 0 * Z.pos d) at 1 by lia. generalize (Z.le_refl 0). generalize 0 at 2 3 4 as offset. revert d x. induction s. reflexivity. intros d x offset oz ex. change (Zseq offset (S s)) with (offset :: Zseq (1 + offset) s). change (existsb ?f (?a :: ?l)) with (f a || existsb f l). simpl mainloop. f_equal. rewrite ex; auto. apply IHs. lia. replace (x * x) with (x ^ 2) by lia. rewrite ex. rewrite 2pow_mod_spec. rewrite <-Zpow_mod. f_equal. rewrite <-!Z.pow_mul_r. rewrite Z.pow_add_r. f_equal. lia. lia. lia. apply Z.mul_nonneg_nonneg; try lia; try (apply Z.pow_nonneg; lia). lia. Qed.
imports: Coq(ZArith Znumtheory Lia Psatz List Bool) Coqtail(Ztools Zeqm Zlittle_fermat Zpow Zprime)