proposition: Lemma reshape_indexK sh i : flatten_index sh (reshape_index sh i) (reshape_offset sh i) = i.
proof: Proof. rewrite /reshape_offset /reshape_index /flatten_index -subSKn. elim: sh => //= n sh IHsh in i *; rewrite subn_eq0; have [//|le_n_i] := ltnP. by rewrite /= subnDA subSn // -addnA IHsh subnKC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)