proposition: Lemma partition_big_fin_img (f : A -> B) g : \big[M/idx]_(i in A) (g i) = \big[M/idx]_(r <- fin_img f) \big[M/idx]_(i in A | f i == r) (g i).
proof: Proof. have /= := @partition_big_undup_map (enum A) f g. rewrite enum_uniq => /(_ isT) H. transitivity (\big[M/idx]_(i <- enum A) g i); first by rewrite enumT. by rewrite H; apply eq_bigr => i _; apply congr_big => //; rewrite enumT. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) logb ssr_ext ssralg_ext