proposition: Lemma edges_atP e z : reflect (e \in eset G /\ exists b, endpt G b e = z) (e \in edges_at G z).
proof: Proof. rewrite edges_atE /incident. apply: (iffP andP); intuition. - case/existsP : H1 => b /eqP<-. by exists b. - case: H1 => b <-. apply/existsP. by exists b. 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)