proposition: Lemma rank_block0dl m n a Aur (Adr : 'M[F]_(m,n)) : a != 0 -> \rank (block_mx (a%:M : 'M_1) Aur 0 Adr) = (1 + \rank Adr)%N.
proof: Proof. move=> nz_a. rewrite /block_mx -addsmxE mxrank_disjoint_sum. rewrite rank_row0mx rank_rV. have->//: row_mx a%:M Aur != 0. apply/eqP => /matrixP/(_ 0 0); rewrite !mxE. by case: splitP => // j _; rewrite ord1 !mxE; move/eqP: nz_a. apply/eqP/rowV0P => v0; rewrite sub_capmx; case/andP=> /sub_rVP [k Hv0k]. rewrite Hv0k; case/submxP => D /matrixP/(_ 0 0); rewrite !mxE. case: splitP => // j _; rewrite ord1 mxE mulr1n big1. by move/eqP; rewrite mulf_eq0 (negbTE nz_a) orbF => /eqP ->; rewrite scale0r. by move=> i _; rewrite !mxE; case: splitP=> // l _; rewrite mxE mulr0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(ssralg fintype fingroup perm) mathcomp(matrix bigop zmodp mxalgebra) gauss