proposition: Lemma sub_minor (S G : sgraph) : subgraph S G -> minor G S.
proof: Proof. move => [h inj_h hom_h]. pose phi x := if @idP (x \in codom h) is ReflectT p then Some (iinv p) else None. exists phi; split. - move => y. exists (h y). rewrite /phi. case: {-}_ / idP => [p|]; by rewrite ?iinv_f ?codom_f. - move => y x0 y0. rewrite !inE {1 2}/phi. case: {-}_ / idP => // p /eqP[E1]. case: {-}_ / idP => // q /eqP[E2]. suff -> : (x0 = y0) by exact: connect0. by rewrite -(f_iinv p) -(f_iinv q) E1 E2. - move => x y A. move/hom_h : (A) => B. exists (h x). exists (h y). rewrite !inE /phi B. + by do 2 case: {-}_ / idP => [?|]; rewrite ?codom_f ?iinv_f ?eqxx //. + apply: contraTneq A => /inj_h ->. by rewrite sgP. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)