proposition: Lemma flatten_indexP sh r c : c < nth 0 sh r -> flatten_index sh r c < sumn sh.
proof: Proof. move=> lt_c_sh; rewrite -[sh in sumn sh](cat_take_drop r) sumn_cat ltn_add2l. suffices lt_r_sh: r < size sh by rewrite (drop_nth 0 lt_r_sh) ltn_addr. by case: ltnP => // le_sh_r; rewrite nth_default in lt_c_sh. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)