proposition: Lemma to_word_filter_nnil t : to_word (filter (fun r => r != [::]) t) = to_word t.
proof: Proof. Proof using. elim: t => [// | t0 t IHt] /=. rewrite to_word_cons -IHt. case: (t0 =P [::]) => [-> | _] /=; first by rewrite cats0. by rewrite to_word_cons. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted