proposition: Lemma sumn_set_nth_ltn s x0 n x : n < size s -> sumn (set_nth x0 s n x) = sumn s + x - nth x0 s n.
proof: Proof. move=> nlts; rewrite sumn_set_nth nlts muln1. have -> : n - size s = 0 by apply/eqP; rewrite subn_eq0 ltnW. by rewrite muln0 addn0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)