proposition: Lemma bool_of_F2K x : bool_of_F2 x = x :> 'F_2.
proof: Proof. rewrite (F2_0_1 x); by case Heq : ( _ == _ ). Qed.
imports: mathcomp(all_ssreflect fingroup perm ssralg zmodp) mathcomp(matrix mxalgebra poly polydiv mxpoly)