proposition: Lemma set_nthE s x0 n x : set_nth x0 s n x = if n < size s then take n s ++ x :: drop n.+1 s else s ++ ncons (n - size s) x0 [:: x].
proof: Proof. elim: s n => [|a s IH] n /=; first by rewrite subn0 set_nth_nil. case: n => [|n]; first by rewrite drop0. by rewrite ltnS /=; case: ltnP (IH n) => _ ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)