proposition: Lemma drop_nth n s : n < size s -> drop n s = nth s n :: drop n.+1 s.
proof: Proof. by elim: s n => [|x s IHs] [|n] Hn //=; rewrite ?drop0 1?IHs. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)