proposition: Lemma bool_of_F2_add_xor x y : bool_of_F2 (x + y) = bool_of_F2 x (+) bool_of_F2 y.
proof: Proof. move: x y; by case/F2P; case/F2P. Qed.
imports: mathcomp(all_ssreflect fingroup perm ssralg zmodp) mathcomp(matrix mxalgebra poly polydiv mxpoly)