proposition: Lemma geometric_partial_tail {R : fieldType} (n m : nat) (x : R) : \sum_(m <= i < m + n) x ^+ i = series (geometric (x ^+ m) x) n.
proof: Proof. by rewrite (big_addn 0 _ m) addnC addnK; under eq_bigr do rewrite exprD mulrC. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau