proposition: Lemma sub_sub (G H : graph) : subgraph G H -> sgraph.subgraph G H.
proof: Proof. case => hv [he] [hd] [hom] [inj_hv inj_he]. exists hv => // x y xy _. move: x y xy. apply skelP; first by move=> x y; rewrite sg_sym. move=> e sNt. rewrite /edge_rel/=/sk_rel (inj_eq inj_hv) sNt. generalize (endpoint_ihom (is_ihom:=hom) e false). generalize (endpoint_ihom (is_ihom:=hom) e true). case (hd e)=>/= <- <-. by rewrite adjacent_sym adjacent_edge. by apply adjacent_edge. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient bij preliminaries) GraphTheory(digraph sgraph treewidth minor checkpoint) GraphTheory(setoid_bigop structures mgraph mgraph2)