proposition: Lemma nth_reshape (sh : seq nat) l n : nth [::] (reshape sh l) n = take (nth 0 sh n) (drop (sumn (take n sh)) l).
proof: Proof. elim: n sh l => [| n IHn] [| sh0 sh] l; rewrite ?take0 ?drop0 //=. by rewrite addnC -drop_drop; apply: IHn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)