proposition: Lemma set_nth_rcons x0 s x n y : set_nth x0 (rcons s x) n y = if n < size s then rcons (set_nth x0 s n y) x else if n == size s then rcons s y else (rcons s x) ++ ncons (n - size s).-1 x0 [:: y].
proof: Proof. Proof using. elim: s n => [// | s0 s IHs] n. - by case eqP => [-> // |]; case: n => [| []]. - rewrite rcons_cons /=; case: n => //= n. move/(_ n) : IHs; rewrite eqSS ltnS. by case (ltngtP n (size s)) => _ <-. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)