proposition: Lemma poly_geom (R : comRingType) n (p : {poly R}) : p ^+ n.+1 - 1 = (p - 1) * \sum_(i < n.+1) p ^+ i.
proof: Proof. rewrite mulrBl mul1r {1}big_ord_recr big_ord_recl /=. rewrite [_ + p^+_]addrC mulrDr -exprS expr0 addrAC opprD addrA mulr_sumr. rewrite (eq_bigr (fun i : 'I_n => p * p ^+ i)) ?subrK // => i _. by rewrite exprS. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)