proposition: Lemma eq_big_idx_seq : forall idx' I r (P : pred I) F, right_unit *%M idx' -> has P r -> \big[*%M/idx']_(i <- r | P i) F i === \big[*%M/1]_(i <- r | P i) F i.
proof: Proof. move=> idx' I r P F op_idx'. rewrite <- !(big_filter r), has_count, count_filter. case/lastP: (filter P r) => {r p}// r i _. rewrite <- cats1, !big_cat_nested; rewrite -> big_cons; rewrite -> big_nil => /=. by rewrite -> op_right_id, op_idx'; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops