proposition: Lemma size_lead_coef_F2 p : size p <> O -> lead_coef p = 1.
proof: Proof. move/eqP => H; apply/eqP; rewrite F2_eq1 lead_coefE; apply: contra H. case: p => p /=; rewrite (nth_last 0 p); by case: p => //= h t /negbTE ->. Qed.
imports: mathcomp(all_ssreflect fingroup perm ssralg zmodp) mathcomp(matrix mxalgebra poly polydiv mxpoly)