proposition: Lemma incident_flip (G : pre_graph) e x : incident (flip_edge G e) x =1 incident G x.
proof: Proof. move => e0. rewrite /incident. case: (altP (e0 =P e)) => [->|D]. - apply/existsP/existsP => [] [b] /eqP<-; exists (~~ b) => /=; by rewrite updateE ?negbK. - apply/existsP/existsP => [] [b] /eqP<-; exists b => /=; by rewrite updateE ?negbK. 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)