proposition: Lemma mulmx_ebase m n (A : 'M_(m, n)) : col_ebase A *m pid_mx (\rank A) *m row_ebase A = A.
proof: Proof. rewrite mxrankE /col_ebase /row_ebase unlock. elim: m n A => [n A | m IHm]; first by rewrite [A]flatmx0 [_ *m _]flatmx0. case=> [A | n]; first by rewrite [_ *m _]thinmx0 [A]thinmx0. rewrite -(add1n m) -?(add1n n) => A /=. case: pickP => [[i0 j0] | A0] /=; last first. apply/matrixP=> i j; rewrite pid_mx_0 mulmx0 mul0mx mxE. by move/eqP: (A0 (i, j)). set a := A i0 j0 => nz_a; set A1 := xrow _ _ _. set u := ursubmx _; set v := _ *: _; set B : 'M_(m, n) := _ - _. move: (rank_leq_col B) (rank_leq_row B) {IHm}(IHm n B); rewrite mxrankE. case: (GaussE B) => [[L U] r] /= r_m r_n defB. have ->: pid_mx (1 + r) = block_mx 1 0 0 (pid_mx r) :> 'M[F]_(1 + m, 1 + n). rewrite -(subnKC r_m) -(subnKC r_n) pid_mx_block -col_mx0 -row_mx0. by rewrite block_mxA castmx_id col_mx0 row_mx0 -scalar_mx_block -pid_mx_block. rewrite xcolE xrowE mulmxA -xcolE -!mulmxA. rewrite !(addr0, add0r, mulmx0, mul0mx, mulmx_block, mul1mx) mulmxA defB. rewrite addrC subrK mul_mx_scalar scalerA divff // scale1r. have ->: a%:M = ulsubmx A1 by rewrite [_ A1]mx11_scalar !mxE !lshift0 !tpermR. rewrite submxK /A1 xrowE !xcolE -!mulmxA mulmxA -!perm_mxM !tperm2 !perm_mx1. by rewrite mulmx1 mul1mx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg finalg zmodp matrix)