proposition: Lemma big_pmap J I (h : J -> option I) (r : seq J) F : \big[op/idx]_(i <- pmap h r) F i = \big[op/idx]_(j <- r) oapp F idx (h j).
proof: Proof. elim: r => [| r0 r IHr]/=; first by rewrite !big_nil. rewrite /= big_cons; case: (h r0) => [i|] /=; last by rewrite mul1m. by rewrite big_cons IHr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)