Coq ssreflect - rewrite inside \big

Question

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 ?

Answer 1

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