proposition: Lemma rank_elimP m n (M : 'M_(m, n)) : rank_elim M = \rank M.
proof: Proof. elim: n m M => [m M|n IHn m]; first by rewrite thinmx0 mxrank0. rewrite -[n.+1]/(1 + n)%N => M /=. rewrite /find_pivot. have [|nz_Mk0] /= := pickP; last first. rewrite -{2}[M]hsubmxK. suff->: lsubmx M = 0 by rewrite rank_row0mx. apply/matrixP => i j; rewrite !mxE ord1 lshift0. by have /(_ i)/negbFE/eqP -> := nz_Mk0. case: m M => [M []|m] //. rewrite -[m.+1]/(1 + m)%N => M k /= nz_Mk0; rewrite IHn. pose P : 'M[F]_(1 + m) := perm_mx (lift_perm 0 k 1%g). have->: \rank M = \rank (P *m M). by rewrite eqmxMfull // row_full_unit unitmx_perm. rewrite -row_permE. set xM : 'M[F]_(1 + m, 1 + n) := row_perm _ _. pose D : 'M[F]_(1 + m) := block_mx 1%:M 0 (- (M k 0)^-1 *: (dlsubmx xM)) 1%:M. have hD : row_full D. by rewrite row_full_unit unitmxE !det_lblock !det1 !mul1r unitr1. rewrite -(eqmxMfull xM hD) -[xM]submxK mulmx_block !mul1mx !mul0mx !addr0. rewrite scaleNr mulNmx [ulsubmx xM]mx11_scalar !mxE !lshift0 lift_perm_id. rewrite mul_mx_scalar scalerA divrr ?unitfE // scale1r addNr rank_block0dl //. rewrite {3}/xM /drsubmx /dlsubmx -row'_row_perm addrC /ursubmx -row_row_perm. by rewrite mulNmx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(ssralg fintype fingroup perm) mathcomp(matrix bigop zmodp mxalgebra) gauss