proposition: Lemma mem_seq_sub_enum x : x \in seq_sub_enum.
proof: Proof. by rewrite mem_undup mem_pmap -valK map_f ?ssvalP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)