proposition: Lemma in_edges (G : sgraph) (u v : G) : [set u; v] \in E(G) = (u -- v).
proof: Proof. apply/edgesP/idP => [[x] [y] []|]; last by exists u; exists v. by case/doubleton_eq_iff => -[-> ->] //; rewrite sgP. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)