proposition: Lemma prim_exp2nS n (w : R) : (2 ^ n.+1).-primitive_root w -> w ^+ (2 ^ n) = -1.
proof: Proof. move=> Hp; have /prim_expr_order/eqP := Hp. rewrite expnS mulnC exprM sqrf_eq1 => /orP[]/eqP // /eqP. by rewrite -(prim_order_dvd Hp) dvdn_Pexp2l // ltnn. Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum) digitn