proposition: Lemma set_nth_non_nil d s n y : set_nth d s n y != [::].
proof: Proof. Proof using. by elim: s => [|s0 s]; case n. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)