proposition: Lemma F2_of_bool_addr x y : x + (y == 0) = ((x + y) == 0).
proof: Proof. case/F2P : x y; case/F2P => //=; by rewrite ?addr0 ?addrr_char2. Qed.
imports: mathcomp(all_ssreflect fingroup perm ssralg zmodp) mathcomp(matrix mxalgebra poly polydiv mxpoly)