proposition: Lemma morph_bool_of_F2 : {morph bool_of_F2 : x y / (x + y) : 'F_2 >-> x (+) y}.
proof: Proof. move=> x y /=; by rewrite bool_of_F2_add_xor. Qed.
imports: mathcomp(all_ssreflect fingroup perm ssralg zmodp) mathcomp(matrix mxalgebra poly polydiv mxpoly)