proposition: Lemma rcs'_rcs (R : idomainType) n (x : 'rV[R]_n.+1) : rcs' x = rcs x.
proof: Proof. rewrite /rcs' /rcs; apply/rowP => i; rewrite !mxE. case: ifPn => [/eqP -> |i0]. congr (x _ _); apply val_inj => /=. by rewrite PermDef.fun_of_permE ffunE /= inordK. congr (x _ _); apply val_inj => /=. rewrite PermDef.fun_of_permE ffunE /= inordK. by rewrite (negPf i0) inordK // (ltn_trans _ (ltn_ord i)) // prednK // lt0n. by rewrite (ltn_trans _ (ltn_ord i)) // prednK // lt0n. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv fingroup perm) mathcomp(finalg zmodp matrix mxalgebra mxpoly polydiv vector) ssralg_ext poly_ext f2 hamming linearcode dft