proposition: Lemma F2_mx_opp m n (a : 'M['F_2]_(m, n)) : - a = a.
proof: Proof. apply/matrixP => i j; by rewrite mxE oppr_char2. Qed.
imports: mathcomp(all_ssreflect fingroup perm ssralg zmodp) mathcomp(matrix mxalgebra poly polydiv mxpoly)