proposition: Lemma rank_row0mx (m n p : nat) (M : 'M[F]_(m,n)) : \rank (row_mx (0: 'M[F]_(m,p)) M) = \rank M.
proof: Proof. by rewrite -mxrank_tr tr_row_mx trmx0 -addsmxE adds0mx mxrank_tr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(ssralg fintype fingroup perm) mathcomp(matrix bigop zmodp mxalgebra) gauss