proposition: Lemma big_enum_rank_cond (I : finType) (A : pred I) z (zA : z \in A) P F (h := enum_rank_in zA) : \big[op/x]_(i < #|A| | P i) F i = \big[op/x]_(s in A | P (h s)) F (h s).
proof: Proof. rewrite big_enum_val_cond {}/h. by apply: eq_big => [i|i Pi]; rewrite ?enum_valK_in. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)