proposition: Lemma eq_big_idx_seq idx' I r (P : pred I) F : right_id idx' *%M -> has P r -> \big[*%M/idx']_(i <- r | P i) F i = \big[*%M/1]_(i <- r | P i) F i.
proof: Proof. move=> op_idx'; rewrite -!(big_filter _ _ r) has_count -size_filter. case/lastP: (filter P r) => {r}// r i _. by rewrite -cats1 !(big_cat_nested, big_cons, big_nil) op_idx' mulm1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)