proposition: Lemma prim_sqr n (w : R) : (2 ^ n.+1).-primitive_root w -> (2 ^ n).-primitive_root (w ^+ 2).
proof: Proof. move=> Hp. have -> : (2 ^ n = 2 ^ n.+1 %/ (gcdn 2 (2 ^ n.+1)))%N. by rewrite -(expn_min _ 1) (minn_idPl _) // expnS mulKn. by rewrite exp_prim_root. Qed.
imports: mathcomp(all_ssreflect all_algebra ssrnum) digitn