proposition: Lemma incident_iso (F G : graph) (h : F ≃ G) (x : F) (e : edge F) : incident x e = incident (h x) (h.e e).
proof: Proof. rewrite /incident. apply/existsP/existsP => [] [b] E; exists (h.d e (+) b). - by rewrite endpoint_iso addbA addbb addFb (eqP E). - by rewrite endpoint_iso bij_eq in E. Qed.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)