proposition: Lemma degree_one_two x y e e1 e2 : e1 != e2 -> edges_at G x = [fset e] -> edges_at G y = [fset e1;e2] -> x != y.
proof: Proof. move => A Ix Iy. apply: contra_neq A => ?;subst y. wlog suff S : e1 e2 Iy / e1 = e. { rewrite (S _ _ Iy). symmetry. apply: S. by rewrite Iy fsetUC. } apply/eqP. by rewrite -in_fset1 -Ix Iy in_fset2 eqxx. 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)