proposition: Lemma sumn_set_nth s x0 n x : sumn (set_nth x0 s n x) = sumn s + x - (nth x0 s n) * (n < size s) + x0 * (n - size s).
proof: Proof. rewrite set_nthE; case: ltnP => [nlts|nges]; last first. by rewrite sumn_cat sumn_ncons /= addn0 muln0 subn0 addnAC addnA. have -> : n - size s = 0 by apply/eqP; rewrite subn_eq0 ltnW. rewrite -[in sumn s](cat_take_drop n s) [drop n s](drop_nth x0)//. by rewrite !sumn_cat /= muln1 muln0 addn0 addnAC !addnA [in RHS]addnAC addnK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)