proposition: Lemma rel_of_pairs_map_eq (H G : eqType) (l : pairs G) (f : G -> H) : injective f -> forall u v, rel_of_pairs l u v = rel_of_pairs (map_pairs f l) (f u) (f v).
proof: Proof. move => f_inj u v. rewrite /rel_of_pairs/= /map_pairs. apply/idP/mapP => [uv_l|[[u' v'] uv_l]]; first by exists (u,v). case. by do 2 move/f_inj ->. Qed.
imports: Coq(RelationClasses Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij finite_quotient)