proposition: Lemma flatten_indexKr sh r c : c < nth 0 sh r -> reshape_offset sh (flatten_index sh r c) = c.
proof: Proof. rewrite /reshape_offset /reshape_index /flatten_index. elim: sh r => [|n sh IHsh] [|r] //= lt_c_sh; first by rewrite ifT ?subn0. by rewrite -addnA -addnS addKn /= subnDl IHsh. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)