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