proposition: Lemma big_uniq (I : finType) (r : seq I) F : uniq r -> \big[op/x]_(i <- r) F i = \big[op/x]_(i in r) F i.
proof: Proof. move=> uniq_r; rewrite -big_enum; apply: perm_big. by rewrite uniq_perm ?enum_uniq // => i; rewrite mem_enum. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)