proposition: Lemma join_width (G1 G2 : sgraph) (D1 : T1 -> {set G1}) (D2 : T2 -> {set G2}) : width (decompU D1 D2) <= maxn (width D1) (width D2).
proof: Proof. apply/bigmax_leqP => [[x|x] _]. all: rewrite /decompU /= card_imset; try solve [exact: inl_inj|exact: inr_inj]. - apply: leq_trans (leq_maxl _ _). exact: leq_bigmax. - apply: leq_trans (leq_maxr _ _). exact: leq_bigmax. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity set_tac)