proposition: Lemma subrX1 x n : x ^+ n - 1 = (x - 1) * (\sum_(i < n) x ^+ i).
proof: Proof. rewrite -!(opprB 1) mulNr -{1}(expr1n _ n). rewrite (subrXX_comm _ (commr_sym (commr1 x))); congr (- (_ * _)). by apply: eq_bigr => i _; rewrite expr1n mul1r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)