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