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