proposition: Lemma count_set_nth_ltn a s x0 n x : n < size s -> count a (set_nth x0 s n x) = count a s + a x - a (nth x0 s n).
proof: Proof. move=> nlts; rewrite count_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)