proposition: Lemma big_enum_rank (I : finType) (A : pred I) x (xA : x \in A) F (h := enum_rank_in xA) : \big[op/idx]_(i < #|A|) F i = \big[op/idx]_(s in A) F (h s).
proof: Proof. by rewrite (big_enum_rank_cond xA) big_mkcondr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)