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