proposition: Lemma prim2_rootN1 (F : fieldType) : 2%:R != 0 :> F -> 2.-primitive_root (- 1 : F).
proof: Proof. move=> tow_neq0; apply/'forall_eqP => -[[|[|]]]//= _; last first. by apply/unity_rootP; rewrite -signr_odd. by apply/unity_rootP/eqP; rewrite expr1 eq_sym -addr_eq0 -mulr2n. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(char0 various)