proposition: Lemma tmp : (d + (n - d.+1).+1 = n)%nat.
proof: Proof. move: dn; rewrite /RS.redundancy_ub => ?. rewrite subnS prednK //; last by rewrite subn_gt0. by rewrite subnKC // ltnW. 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