proposition: Lemma bijective_F2_of_bool : {on [pred i in 'F_2], bijective F2_of_bool}.
proof: Proof. exists bool_of_F2; move=> x Hx /=; by rewrite ?F2_of_boolK ?bool_of_F2K. Qed.
imports: mathcomp(all_ssreflect fingroup perm ssralg zmodp) mathcomp(matrix mxalgebra poly polydiv mxpoly)