proposition: Lemma edges_at_iso (F G : graph) (h : F ≃ G) (x : F) : edges_at (h x) = [set h.e e | e in edges_at x].
proof: Proof. apply/setP => e. by rewrite -[e](bijK' h.e) bij_imset_f !inE (incident_iso h). Qed.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)