proposition: Lemma size_integ_eq0 (p : {poly K}) : (forall i, 0 <= p`_i) -> size (integ p) == O -> size p == O.
proof: Proof. move=> p0. rewrite size_poly_eq0 => /eqP Hip. have : (integ p)`_(size p).-1 == 0 by rewrite Hip coef0. rewrite /integ coef_poly. case/boolP : (size p > 0)%nat => [Hp|]. rewrite prednK // leqnn. case/boolP : (p`_(size p).-1 > 0) => [Hp'|]. move: Hp. rewrite -(ltr0n K) => /(divr_gt0 Hp') H1 /eqP H2. by rewrite H2 ltxx in H1. rewrite lt_def p0 andbT negbK lead_coef_eq0 => /eqP ->. by rewrite size_poly0. by rewrite lt0n negbK. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist