proposition: Lemma prim_order_exists n z : n > 0 -> z ^+ n = 1 -> {m | m.-primitive_root z & (m %| n)}.
proof: Proof. move=> n_gt0 zn1. have: exists m, (m > 0) && (z ^+ m == 1) by exists n; rewrite n_gt0 /= zn1. case/ex_minnP=> m /andP[m_gt0 /eqP zm1] m_min. exists m. apply/andP; split=> //; apply/eqfunP=> [[i]] /=. rewrite leq_eqVlt unity_rootE. case: eqP => [-> _ | _]; first by rewrite zm1 eqxx. by apply: contraTF => zi1; rewrite -leqNgt m_min. have: n %% m < m by rewrite ltn_mod. apply: contraLR; rewrite -lt0n -leqNgt => nm_gt0; apply: m_min. by rewrite nm_gt0 /= expr_mod ?zn1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)