proposition: Lemma count_set_nthF a s x0 n x : ~~ a x0 -> count a (set_nth x0 s n x) = count a s + a x - a (nth x0 s n).
proof: Proof. move=> /negbTE ax0; rewrite count_set_nth ax0 mul0n addn0. case: ltnP => [_|nges]; first by rewrite muln1. by rewrite nth_default// ax0 subn0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)