proposition: Lemma units_Zp_cyclic p : prime p -> cyclic (units_Zp p).
proof: Proof. by move/pdiv_id <-; exact: field_unit_group_cyclic. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice div) mathcomp(fintype bigop prime finset fingroup morphism) mathcomp(perm automorphism quotient gproduct ssralg) mathcomp(finalg zmodp poly)