proposition: Lemma sum_coef_pos (K : numFieldType) (p : DegreeDistribution.Lambda K) : p.[1] > 0.
proof: Proof. destruct p. have p0pos : 0 <= sum_coef p by apply sumr_ge0. rewrite -sum_coef_horner lt0r /= p0pos andbT. apply: contra psize => /eqP sum0. rewrite size_poly_eq0 -lead_coef_eq0 /lead_coef. case/boolP : ((size p).-1 < size p)%nat => [H|]. apply/eqP; apply: (@psumr_eq0P K _ xpredT _ _ sum0 (Ordinal H) erefl) => ? _. by apply p0. rewrite -leqNgt => ?. by rewrite nth_default. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist