proposition: Lemma rel_of_pairs_mapE (H G : eqType) (l : pairs G) (f : G -> H) (u' v' : H) : rel_of_pairs (map_pairs f l) u' v' -> exists u v : G, u' = f u /\ v' = f v.
proof: Proof. rewrite /rel_of_pairs/= /map_pairs. case/mapP => [[u v]] /= ? [? ?]. by exists u; exists v. Qed.
imports: Coq(RelationClasses Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij finite_quotient)