proposition: Lemma mem_to_word t rc : in_shape (shape t) rc -> get_tab t rc \in (to_word t).
proof: Proof. Proof using. move: rc => [r c]; rewrite /in_shape /get_tab. elim: t r c => [// | t0 t IHt] /= r c; first by rewrite nth_default. rewrite to_word_cons mem_cat => H. case: r H => [/mem_nth ->| r] /=; first by rewrite orbT. by move/IHt ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted