proposition: Lemma filter_to_word t p : filter p (to_word t) = to_word (map (filter p) t).
proof: Proof. Proof using. elim: t => [// | t0 t IHt] /=. by rewrite !to_word_cons -IHt filter_cat. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted