proposition: Lemma count_unionP x : P x -> count_mem x enum_union = 1.
proof: Proof. Proof using HPTi Hpart. move=> HPx; have:= HPx; rewrite /enum_union => /Hpart H. rewrite count_flatten -2!map_comp. pose ix := @Sub TI PI TPI (FI x) H. rewrite (eq_map (g := fun i => i == ix : nat)); first last. move=> i /=. case: eqP => [->{i} | Hneq]. - rewrite count_map /=. have Hix : Pi (val ix) x by rewrite -HPTi /= SubK HPx eq_refl. pose xPI := @Sub T _ (TPi ix) x Hix. rewrite (eq_count (a2 := pred1 xPI)); first last. move=> y /=; apply/eqP/eqP => HH. + by apply val_inj; rewrite HH SubK. + by rewrite HH SubK. by rewrite enumT /=; exact: (@enumP (TPi ix)). - apply/count_memPn; apply/contra_notN: Hneq => /mapP[xfin _ Hx]. apply val_inj; rewrite SubK. by have:= valP xfin; rewrite /= -HPTi Hx=> /andP[_ /eqP->]. by rewrite sumn_count /=; exact: (@enumP TPI). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools