proposition: Lemma nth_set_nth_any a b l i c j : nth a (set_nth b l i c) j = if j == i then c else if j < size l then nth a l j else if j <= i then b else a.
proof: Proof. Proof using. case eqP => [<- | /eqP Hneq]. - have Hj : j < size (set_nth b l j c) by rewrite size_set_nth; apply: leq_maxl. by rewrite (set_nth_default b a Hj) nth_set_nth /= eq_refl. - case (ltnP j (size l)) => Hjsz. + have Hj : j < size (set_nth b l i c) by rewrite size_set_nth; apply: (leq_trans Hjsz); apply: leq_maxr. rewrite (set_nth_default b a Hj) nth_set_nth /= (negbTE Hneq). exact: set_nth_default. + case (leqP j i) => Hij. * by apply: nth_set_nth_expand; rewrite Hjsz /= ltn_neqAle Hneq Hij. * rewrite nth_default; first by []. by rewrite size_set_nth /maxn; case (ltnP i.+1 (size l)). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)