proposition: Lemma drop_index s (n := index x0 s) : x0 \in s -> drop n s = x0 :: drop n.+1 s.
proof: Proof. by move=> xs; rewrite (drop_nth x0) ?index_mem ?nth_index. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)