proposition: Lemma rename_width (T : forest) (G : sgraph) (D : T -> {set G}) (G' : finType) (h : G -> G') : width (rename D h) <= width D.
proof: Proof. apply: bigmax_leq_pointwise => t _. exact: leq_imset_card. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity set_tac)