proposition: Lemma GF2_of_F2_eq0 x : (GF2_of_F2 x == 0) = (x == 0).
proof: Proof. apply/idP/idP => [|/eqP -> //]. rewrite /GF2_of_F2 /=; case: ifPn => //; rewrite -F2_eq1 => ->. by rewrite oner_eq0. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2 mathcomp(finfield)