proposition: Lemma eq_big_idx idx' (I : finType) i0 (P : pred I) F : P i0 -> right_id idx' *%M -> \big[*%M/idx']_(i | P i) F i = \big[*%M/1]_(i | P i) F i.
proof: Proof. by move=> Pi0 op_idx'; apply: eq_big_idx_seq => //; apply/hasP; exists i0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)