proposition: Lemma expgS x n : x ^+ n.+1 = x * x ^+ n.
proof: Proof. by case: n => //; rewrite mulg1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)