proposition: Lemma F2_addmx0 m n (a b : 'M['F_2]_(m, n)) : a + b = 0 -> a = b.
proof: Proof. by move/eqP; rewrite addr_eq0 F2_mx_opp => /eqP. Qed.
imports: mathcomp(all_ssreflect fingroup perm ssralg zmodp) mathcomp(matrix mxalgebra poly polydiv mxpoly)