proposition: Lemma sumn_set_nth0 s n x : sumn (set_nth 0 s n x) = sumn s + x - nth 0 s n.
proof: Proof. rewrite sumn_set_nth mul0n addn0. by case: ltnP => [_|nges]; rewrite ?muln1// nth_default. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)