proposition: Lemma reshape_offsetP sh i : i < sumn sh -> reshape_offset sh i < nth 0 sh (reshape_index sh i).
proof: Proof. rewrite /reshape_offset /reshape_index; elim: sh => //= n sh IHsh in i *. rewrite subn_eq0; have [| le_n_i] := ltnP i n; first by rewrite subn0. by rewrite -leq_subLR /= subnDA subSn // => /IHsh. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)