proposition: Lemma tree'_of_trace_deg l pn (seqs : l.*2.+1.-tuple _) : (max_deg (tree'_of_trace pn seqs) <= #|port|)%nat.
proof: Proof. rewrite max_deg_all. rewrite size_map -cardE max_card andTb. apply/allP => t /mapP [p Hp ->] {t pn Hp}. apply tree_of_trace_deg. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner