proposition: Lemma base_full : row_full base.
proof: Proof. rewrite /row_full (eqnP base_free) /nA; case: ex_maxnP => nA. case/existsP=> /= B /eqnP Bfree nA_max; rewrite -Bfree eqn_leq rank_leq_col. rewrite -{1}(mxrank1 F n) mxrankS //; apply/row_subP=> j; set u := row _ _. move/implyP: {nA_max}(nA_max nA.+1); rewrite ltnn implybF. apply: contraR => nBj; apply/existsP. exists (row_mx (const_mx j : 'M_1) B); rewrite -row_leq_rank. pose Bj := Ad *m lin1_mx (mulmx u \o vec_mx). have rBj: \rank Bj = d. apply/eqP; rewrite eqn_leq rank_leq_row -subn_eq0 -mxrank_ker mxrank_eq0 /=. apply/rowV0P=> v /sub_kermxP; rewrite mulmxA mul_rV_lin1 /=. rewrite -horner_rVpoly; pose x := inFA v; rewrite -/(mxval x). have [[] // | nzx /(congr1 (mulmx^~ (mxval x^-1)))] := eqVneq x 0. rewrite mul0mx /= -mulmxA -mxvalM divff // mxval1 mulmx1. by move/rowP/(_ j)/eqP; rewrite !mxE !eqxx oner_eq0. rewrite {1}mulSn -Bfree -{1}rBj {rBj} -mxrank_disjoint_sum. rewrite mxrankS // addsmx_sub -[nA.+1]/(1 + nA)%N; apply/andP; split. apply/row_subP=> k; rewrite row_mul mul_rV_lin1 /=. apply: eq_row_sub (mxvec_index (lshift _ 0) k) _. by rewrite !rowK mxvecK mxvecE mxE row_mxEl mxE -row_mul mul1mx. apply/row_subP; case/mxvec_indexP=> i k. apply: eq_row_sub (mxvec_index (rshift 1 i) k) _. by rewrite !rowK !mxvecE 2!mxE row_mxEr. apply/eqP/rowV0P=> v; rewrite sub_capmx => /andP[/submxP[w]]. set x := inFA w; rewrite {Bj}mulmxA mul_rV_lin1 /= -horner_rVpoly -/(mxval x). have [-> | nzx ->] := eqVneq x 0; first by rewrite mxval0 mulmx0. move/(submxMr (mxval x^-1)); rewrite -mulmxA -mxvalM divff {nzx}//. rewrite mxval1 mulmx1 => Bx'j; rewrite (submx_trans Bx'j) in nBj => {Bx'j} //. apply/row_subP; case/mxvec_indexP=> i k. rewrite row_mul rowK mxvecE mxE rowE -mulmxA. have ->: A ^+ k *m mxval x^-1 = mxval (groot ^+ k / x). by rewrite mxvalM rmorphXn /= mxval_groot. rewrite [mxval _]horner_rVpoly; move: {k u x}(val _) => u. rewrite (mulmx_sum_row u) !linear_sum summx_sub //= => k _. rewrite !linearZ scalemx_sub //= rowK mxvecK -rowE. by apply: eq_row_sub (mxvec_index i k) _; rewrite rowK mxvecE mxE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv finset fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup matrix mxalgebra) mathcomp(mxpoly)