proposition: Lemma big_enum_val_cond (I : finType) (A : pred I) (P : pred I) F : \big[op/x]_(x in A | P x) F x = \big[op/x]_(i < #|A| | P (enum_val i)) F (enum_val i).
proof: Proof. have [A_eq0|/card_gt0P[x0 x0A]] := posnP #|A|. rewrite !big_pred0 // => i; last by rewrite card0_eq. by have: false by move: i => []; rewrite A_eq0. rewrite (reindex (enum_val : 'I_#|A| -> I)). by apply: eq_big => [y|y Py]; rewrite ?enum_valP. by apply: subon_bij (enum_val_bij_in x0A) => y /andP[]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)