proposition: Lemma add_edge_subgraph (G : sgraph) (x y : G) : subgraph G (add_edge x y).
proof: Proof. by exists id => // u v uv _; rewrite /edge_rel/= uv. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)