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