proposition: Lemma RS_min_dist1 c : n.-primitive_root a -> c != 0 -> c \in RS.code a n d -> d.+1 <= wH c.
proof: Proof. move=> an c0 Hc. have a_neq0 := primitive_uroot_neq0 an. rewrite -(wH_phase_shift a_neq0 _ d). apply: (@BCH_argument_lemma _ _ (@GRing.idfun_rmorphism F) _ RS_Hchar _ an (phase_shift a c d.+1) _ dn). by rewrite -wH_eq0 wH_phase_shift // wH_eq0. rewrite (_ : \row_i0 (GRing.idfun_rmorphism F) ((phase_shift a c d.+1) ``_ i0) = phase_shift a c d.+1); last by apply/rowP => i; rewrite !mxE. apply (dft_shifting a_neq0 (prim_expr_order an) dn) => i /andP[ir1 ir2]. have {Hc} : c \in RS.codebook a n' d by rewrite -(RS.lcode0_codebook a dn) inE. rewrite inE => /forallP/(_ (Ordinal ir2)) /=. by rewrite ir1 implyTb !mxE => /eqP. 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