proposition: Lemma incident_flip_edge G e x u y : incident (G ∔ [e, x, u, y]) =2 incident (G ∔ [e, y, u°, x]).
proof: Proof. move => z f. rewrite /incident/= !existsb_case. case: (altP (f =P e)) => [->|?]; by rewrite !updateE // orbC. Qed.
imports: HB(structures) Coq(Relation_Definitions Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom rewriting) GraphTheory(finmap_plus)