proposition: Lemma size_integ p : size (integ_deg p) = size p.
proof: Proof. destruct p => /=. rewrite size_poly_eq // prednK ?lt0n // lt0r_neq0 // divr_gt0 //. by rewrite lt0r p0 andbT lead_coef_eq0 -size_poly_eq0. by rewrite ltr0n lt0n. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist