proposition: Lemma sum_powers_of_x (n: nat) (x:R): (x-1) * (\sum_(i < n) x^+ i) = x ^+ n - 1.
proof: Proof. elim: n => [| n Ihn]. by rewrite big_ord0 expr0 mulr0 subrr. rewrite (big_ord_recr n) /= mulrDr Ihn mulrBl mul1r - exprS. by rewrite addrAC addrCA subrr addr0. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)