# Coq ssreflect - rewrite inside \big

I'm trying to prove the following lemma :

Definition SequenceSum {K : fieldType} (s : nat -> K) (n : nat) := \sum_(0 <= i < n.+1) s i.

Lemma one_minus_q_product_development {K : fieldType} (q : K) (n : nat) : (1-q) * SequenceSum (fun (i:nat) => q^+i) n = 1 - q^+(n+1).


I have currently done this :

Proof.
rewrite /SequenceSum mulrBl.
rewrite {1}big_nat_recl//.
rewrite sum_distrr.
rewrite big_nat_recr//.


So the current goal is :

  K : fieldType
q : K
n : nat
============================
1 * (q ^+ 0 + \sum_(0 <= i < n) q ^+ i.+1) - GRing.add_monoid K (\big[GRing.add_monoid K/0]_(0 <= i < n) (q * q ^+ i)) (q * q ^+ n) = 1 - q ^+ (n + 1)


I'm seeking to use the exprS : forall (R : ringType) (x : R) (n : nat), x ^+ n.+1 = x * x ^+ n in order to turn the q * q +^ i into q ^+ i.+1, but upon using rewrite -exprS, it only rewrites the q * q ^+ n (note that it is outside of any \sum) into q ^+ n.+1.

rewrite -2!exprS yields the following error :

Error: At iteration 2: The RHS of exprS
(_ * _ ^+ _)
does not match any subterm of the goal


Despite q * q +^ i being in the goal.

Any ideas on how to use this lemma in order to rewrite a term inside a \sum ?

In this file you'll see examples of using under eq_bigr ... do ... which is how you do such inside rewrites.