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