proposition: Lemma iso_subgraph (G H : sgraph) : diso G H -> subgraph G H.
proof: Proof. case => g E _. exists g. apply (can_inj (bijK g)). move=> x y e _. by apply E. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)