proposition: Lemma rcs'0 (R : idomainType) n (x : 'rV[R]_n.+1) : (rcs' x == 0) = (x == 0).
proof: Proof. apply/idP/idP => [|/eqP ->]. move/eqP/rowP => H; apply/eqP/rowP => i; rewrite !mxE. have ni : i.+1 %% n.+1 < n.+1 by apply ltn_pmod. move: (H (Ordinal ni)); rewrite !mxE -val_eqE /=. case: ifPn => [in' Hx|in' Hx]. have ? : n = i. case/dvdnP : in' => -[//|[|k abs]] /=; last first. exfalso; move: (ltn_ord i); rewrite ltnNge => /negP; apply. by rewrite -ltnS abs ltn_Pmull. by rewrite mul1n => /eqP; rewrite eqSS => /eqP. rewrite -[RHS]Hx; congr (x _ _); apply/val_inj => /=; by rewrite inordK. rewrite -[RHS]Hx modn_small /=; last first. rewrite ltnS ltn_neqAle -ltnS (ltn_ord i) andbT; apply/eqP => in''. by rewrite in'' modnn eqxx in in'. congr (x _ _); apply val_inj => /=; by rewrite inordK. apply/eqP/rowP => i; rewrite !mxE; by case: ifPn. 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