proposition: Lemma nth_flatten x0 ss i (r := reshape_index (shape ss) i) : nth x0 (flatten ss) i = nth x0 (nth [::] ss r) (reshape_offset (shape ss) i).
proof: Proof. rewrite /reshape_offset -subSKn {}/r /reshape_index. elim: ss => //= s ss IHss in i *; rewrite subn_eq0 nth_cat. by have [//|le_s_i] := ltnP; rewrite subnDA subSn /=. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)