proposition: Lemma primitive_root_eq0 (F : fieldType) n (w : F) : n.-primitive_root w -> (w == 0) = (n == 0%N).
proof: Proof. move=> wp; apply/eqP/idP => [w0|/eqP p0]; move: wp; rewrite ?w0 ?p0; last first. by move=> /prim_order_gt0//. move=> /prim_expr_order/esym/eqP. by rewrite expr0n; case: (n =P 0%N); rewrite ?oner_eq0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)