proposition: Lemma same_oarc e x y x' y' u u' : oarc G e x u y -> oarc G e x' u' y' -> [/\ x = x', y = y' & u ≡ u'] \/ [/\ x = y', y = x' & u ≡ u'°].
proof: Proof. case => Ee [b] [A B C]. case => _ [b'] [A' B' C']. case: (altP (b =P b')) => [Eb|]. - subst. left. split => //. apply: eqvbN. apply: eqvb_transR C'. by symmetry. - rewrite -eqb_negR => /eqP ?; subst. right; split => //. by rewrite negbK. apply: eqvbT. apply: eqvb_transR C'. by symmetry. 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)