proposition: Lemma tree_of_graph_deg l k c p : (max_deg (tree_of_graph l k c p) <= #|port|)%nat.
proof: Proof. elim: l k c p => // l IH k c p. rewrite max_deg_all. rewrite size_map -cardE max_card andTb. by apply/allP => t /mapP [p' Hp' ->] {t}. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner