proposition: Lemma rank_GRS_PCM (b : 'rV[F]_n) (rn : r <= n) (b0 : forall i, b ``_i != 0) : \rank (GRS.PCM a b r) = r.
proof: Proof. set lhs := GRS.PCM _ _ _. set lhs' := castmx (erefl r, esym (subnKC rn)) lhs. set K1 := lsubmx lhs'. set K2 := rsubmx lhs'. rewrite -(mxrank_castmx lhs (erefl r) (esym (subnKC rn))). rewrite -/lhs' -(hsubmxK lhs') rank_row_mx //. suff -> : lsubmx lhs' = GRS_PCM_sq a b r by rewrite rank_GRS_PCM_sq. rewrite /lhs' /lhs GRS_PCM_sq_vander //. apply/matrixP => i j. rewrite !mxE castmxE !mxE /=. rewrite (bigID (fun x : 'I_n => x < r) xpredT) /=. rewrite [in X in _ + X = _](eq_bigr (fun=> 0)); last first. move=> k kj; rewrite !mxE esymK (_ : _ == _ = false). by rewrite mulr0n mulr0. apply/negbTE; by apply: contra kj => /eqP -> /=. rewrite big_const iter_addr0 addr0. rewrite big_ord_narrow //. apply eq_bigr => k _. rewrite !mxE /=. rewrite (_ : widen_ord _ _ = inord k); last first. apply val_inj => /=; by rewrite inordK // (leq_trans (ltn_ord k)). congr (_ * (_ *+ nat_of_bool _)). rewrite esymK. apply/idP/idP => [|/eqP ->]; last first. apply/eqP/val_inj => /=. by rewrite inordK // (leq_trans (ltn_ord j)). move/eqP/(congr1 (@nat_of_ord n)). rewrite inordK; last by rewrite (leq_trans (ltn_ord k)). move=> Hk. apply/eqP/ord_inj; by rewrite Hk. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly vector mxalgebra zmodp) ssr_ext ssralg_ext vandermonde linearcode dft poly_decoding