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
?