proposition: Lemma ordered_rmap (G H : sgraph) (phi : H -> {set G}) (m : H -> nat) : injective m -> [/\ forall x : H, phi x != set0, forall x : H, sgraph.connected (phi x), forall x y : H, m x < m y -> x != y -> [disjoint phi x & phi y] & forall x y : H, m x < m y -> x -- y -> neighbor (phi x) (phi y)] -> minor_rmap phi.
proof: Proof. move => inj_m [P1 P2 P3 P4]; split => //. - move => i j iNj. wlog iltj: i j iNj / m i < m j; last exact: P3. move => W. case: (ltngtP (m i) (m j)) => [||E]. + exact: W. + by rewrite disjoint_sym; apply: W; rewrite eq_sym. + apply: contra_neqT iNj => _. exact: inj_m E. - move => i j iNj. wlog iltj: i j iNj / m i < m j; last exact: P4. move => W. case: (ltngtP (m i) (m j)) => [||E]. + exact: W. + by rewrite neighborC; apply: W; rewrite sgP. + apply: contraTT iNj => _. by rewrite (inj_m _ _ E) sgP. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)