proposition: Lemma RS_enc_discard_is_id : cancel_on (RS.code a n d) encoder RS_discard.
proof: Proof. move=> /= c Hc. rewrite /RS_discard -/(high c); apply RS_enc_surjective. by rewrite -RS.lcode0_codebook // ?inE. 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