proposition: Lemma sum_lambda_pred L : (size lambda <= L)%nat -> \sum_(j < L.+1 | j != 0) lambda`_j.-1 = 1.
proof: Proof. move=> HL. transitivity (\sum_(0 <= j < L.+1 | j != 0%nat ) lambda`_j.-1). by rewrite big_mkord. rewrite (@big_cat_nat _ _ _ 1%nat) //=. rewrite big1_seq //; last first. move=> j /andP [Hj] /=. rewrite in_cons in_nil orbF => Hj'. by rewrite Hj' in Hj. rewrite add0r big_add1 /=. move: (NormalizedDegreeDistribution.p1 lambda). rewrite sum_poly_weaken // -sum_coef_horner /sum_coef => <-. by destruct lambda. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner