proposition: Lemma F2P x : F2_spec x (x == 0) (x == 1).
proof: Proof. case/boolP : (x == 0) => [/eqP -> | ]; first by constructor. rewrite F2_eq0 negbK => /eqP ->; by constructor. Qed.
imports: mathcomp(all_ssreflect fingroup perm ssralg zmodp) mathcomp(matrix mxalgebra poly polydiv mxpoly)