proposition: Lemma nthK s: uniq s -> {in gtn (size s), cancel (nth s) (index^~ s)}.
proof: Proof. elim: s => //= x s IHs /andP[s'x Us] i; rewrite inE ltnS eq_sym -if_neg. by case: i => /= [_|i lt_i_s]; rewrite ?eqxx ?IHs ?(memPn s'x) ?mem_nth. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)