proposition: Lemma nth_set_nth_expand a b l i c j : (size l <= j < i) -> nth a (set_nth b l i c) j = b.
proof: Proof. Proof using. elim: l i j => [/= | l0 l IHl]. - elim => [// | i' Hi] /=. by case => [// | j /=]; rewrite nth_ncons /leq subSS => ->. - elim => [// | i' Hi] j /=; first by rewrite ltn0 andbF. case: j Hi => [// | j /=] Hi /andP[H1 H2]. by apply: IHl; move: H1 H2; rewrite !/leq !subSS => -> ->. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)