proposition: Lemma tag_enumP : Finite.axiom tag_enum.
proof: Proof. case=> i x; rewrite -(enumP i) /tag_enum -enumT. elim: (enum I) => //= j e IHe. rewrite count_cat count_map {}IHe; congr (_ + _). rewrite -size_filter -cardE /=; case: eqP => [-> | ne_j_i]. by apply: (@eq_card1 _ x) => y; rewrite -topredE /= tagged_asE ?eqxx. by apply: eq_card0 => y. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)