proposition: Lemma order_Zp1 : #[Zp1] = p.
proof: Proof. by rewrite orderE -Zp_cycle cardsT card_ord. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool choice eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup) mathcomp(ssralg finalg countalg)