proposition: Lemma oppr_closed : oppr_closed codebook.
proof: Proof. move=> /= c; rewrite inE => /forallP H. rewrite inE; apply/forallP => i; apply/implyP => i0. rewrite fdcoorN eqr_oppLR oppr0; move: (H i); by rewrite i0 implyTb. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly vector mxalgebra zmodp) ssr_ext ssralg_ext poly_ext channel_code decoding linearcode hamming dft poly_decoding euclid grs cyclic_code