proposition: Lemma big_bij_eq (T : comMonoid) (I1 I2 : finType) (F : I1 -> T) (f : bij I1 I2) (y : I2) : \big[cm_op/1%CM]_(x | f x == y) F x ≡ F (f^-1 y).
proof: Proof. apply: big_pred1 => x /=. exact: bij_eqLR. Qed.
imports: HB(structures) Coq(RelationClasses Morphisms Relation_Definitions) mathcomp(all_ssreflect) GraphTheory(edone preliminaries setoid_bigop bij)