proposition: Lemma eq_big_idx : forall idx' (I : finType) i0 (P : pred I) F, P i0 -> right_unit *%M idx' -> \big[*%M/idx']_(i | P i) F i === \big[*%M/1]_(i | P i) F i.
proof: Proof. move=> idx' I i0 P F op_idx' Pi0; apply: eq_big_idx_seq => //. by apply/hasP; exists i0; first rewrite /index_enum -enumT mem_enum. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops