proposition: Lemma RS_not_trivial : not_trivial (RS.code a n d).
proof: Proof. rewrite /not_trivial. exists (poly_rV (rs_gen a d)); apply/andP; split. - by rewrite mem_rs_gen_RS. - apply/negP => /poly_rV_0_inv. rewrite size_rs_gen => /(_ dn). apply/negP; by rewrite gen_neq0. 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