proposition: Lemma width_bound (T G : finType) (D : T -> {set G}) : width D <= #|G|.
proof: Proof. apply/bigmax_leqP => t _; exact: max_card. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)