proposition: Lemma iso_strict_minor (G H : sgraph) : diso G H -> strict_minor H G.
proof: Proof. move=> [[h g hgK ghK] /= hH gH]. have in_preim_g x y : (y \in g @^-1 x) = (y == h x). rewrite -mem_preim; exact: can2_eq. exists g; split. + by move=> y; exists (h y); rewrite hgK. + move=> y x1 x2. rewrite !in_preim_g => /eqP-> /eqP->. exact: connect0. + move=> x y xy. exists (h x); exists (h y). rewrite !in_preim_g. split=> //. exact: hH. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)