proposition: Lemma max_deg_all (xs : seq (tree l (negk k))) : ((max_deg (Node xs) <= n) = (size xs <= n) && all (fun x => (max_deg x <= n)) xs)%nat.
proof: Proof. by rewrite /= foldr_maxnE all_map. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist