proposition: Lemma minor_map_comp (G H K : sgraph) (f : G -> option H) (g : H -> option K) : minor_map f -> minor_map g -> minor_map (obind g \o f).
proof: Proof. move=> [f1 f2 f3] [g1 g2 g3]. rewrite /comp; split. - move => y. case: (g1 y) => y'. case: (f1 y') => x E1 ?. exists x. by rewrite E1. - move => z x y. rewrite !inE. case Ef : (f x) => [fx|] //= gfx. case Eg : (f y) => [fy|] //= gfy. move: (g2 z fx fy). rewrite !inE. case/(_ _ _)/Wrap => // /connectP => [[p]]. elim: p x fx Ef gfx => /= [|a p IH] x fx Ef gfx. + move => _ ?. subst fy. move: (f2 fx x y). rewrite !inE Ef Eg. case/(_ _ _)/Wrap => //. apply: connect_mono => a b /=. rewrite !inE -andbA. case/and3P => /eqP-> /eqP-> -> /=. by rewrite (eqP gfx) !eqxx. + rewrite !inE -!andbA => /and4P [H1 H2 H3 H4] H5. case: (f1 a) => x' Hx'. apply: (connect_trans (y := x')); last exact: IH H5. move/f3 : (H3) => [x0] [y0] [X1 X2 X3]. apply: (connect_trans (y := x0)); last apply: (connect_trans (y := y0)). * move: (f2 fx x x0). rewrite !inE ?Ef ?eqxx in X1 *. case/(_ _ _)/Wrap => //. apply: connect_mono => u v /=. rewrite !inE -andbA. case/and3P => /eqP-> /eqP-> -> /=. by rewrite H1. * apply: connect1. rewrite /= !inE ?X3 ?andbT in X1 X2 *. by rewrite (eqP X1) (eqP X2) /= (eqP gfx) eqxx. * move: (f2 a y0 x' X2). case/(_ _)/Wrap. by rewrite !inE Hx'. apply: connect_mono => u v /=. rewrite !inE -andbA. case/and3P => /eqP-> /eqP-> -> /=. by rewrite H2. - move => x y /g3 [x'] [y'] [Hx' Hy'] /f3 [x0] [y0] [Hx0 Hy0 ?]. exists x0. exists y0. rewrite !inE in Hx' Hy' Hx0 Hy0 *. split => //; reflect_eq; by rewrite (Hx0,Hy0) /= (Hx',Hy'). Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)