proposition: Lemma size_to_word t : size (to_word t) = size_tab t.
proof: Proof. Proof using. rewrite /size_tab; elim: t => [// | t0 t IHt] /=. by rewrite to_word_cons size_cat IHt addnC. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted