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
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: Dec 07 2023 at 17:01 UTC