proposition: Lemma F2_poly_add p : p + p = 0.
proof: Proof. apply/polyP => i; by rewrite coef0 coef_add_poly addrr_char2. Qed.
imports: mathcomp(all_ssreflect fingroup perm ssralg zmodp) mathcomp(matrix mxalgebra poly polydiv mxpoly)