proposition: Lemma eq_from_nth_notin x0 s1 s2 : x0 \notin s1 -> x0 \notin s2 -> (forall i : nat, nth x0 s1 i = nth x0 s2 i) -> s1 = s2.
proof: Proof. wlog Hpq : s1 s2 / (size s1) <= (size s2). move=> Hwlog; case: (leqP (size s1) (size s2)); first exact: Hwlog. by move=> /ltnW/Hwlog H +{}/H => +H => {}/H Heq Hnth; rewrite Heq. move=> x0s1 x0s2 Heq; apply: (eq_from_nth (x0 := x0))=> [|i _ //]. apply anti_leq; rewrite {}Hpq/=. case: s2 x0s2 Heq => [//|h2 s2'] Hnotin Heq. apply/contraR: Hnotin; rewrite -ltnNge => Habs. move/(_ (size (h2 :: s2')).-1): Heq; rewrite nth_last. rewrite nth_default => [-> /=|]; first exact: mem_last. by move: Habs; rewrite /= ltnS. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)