proposition: Lemma size1_polyC_F2 p : size p = 1%nat -> p = 1%:P.
proof: Proof. move=> H. by rewrite (@size1_polyC _ p) ?H // -(@size_lead_coef_F2 p) ?H // lead_coefE H. Qed.
imports: mathcomp(all_ssreflect fingroup perm ssralg zmodp) mathcomp(matrix mxalgebra poly polydiv mxpoly)