proposition: Lemma tree_of_trace_deg l k p (seqs : l.-tuple _) : (max_deg (tree_of_trace k p seqs) <= #|port|)%nat.
proof: Proof. elim: l k p seqs => //= l IH k p seqs. destruct ((thead seqs) p) as [ep en]. 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