I had to prove the following lemma, and thought it might interesting to extend `bigop`

with it?

```
Lemma sumn_set_nthE (s : seq nat) x0 n x:
let: x' := if n < size s
then x
else nth x0 s n + sumn (ncons (n - size s) x0 [::x]) in
sumn (set_nth x0 s n x) = sumn s + x' - nth x0 s n.
```

Would a PR be useful for this simple lemma?

A nicer version is the following :

```
Lemma sumn_set_nthE (s : seq nat) x0 n x :
let x' := x + (size s <= n) * (nth x0 s n + (n - size s) * x0) in
sumn (set_nth x0 s n x) = sumn s + x' - nth x0 s n.
```

which comes with the side lemma `sumn_nconsE`

:

```
Lemma sumn_nconsE n s (x0 : nat) : sumn (ncons n x0 s) = n * x0 + sumn s.
```

Pierre Jouvelot has marked this topic as resolved.

Last updated: May 31 2023 at 03:30 UTC