proposition: Lemma rcons_set_nth a s l : set_nth a s (size s) l = rcons s l.
proof: Proof. Proof using. by elim: s => // l0 s IHs; rewrite rcons_cons -IHs. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)