proposition: Lemma row'_row_perm m n M k : row' k M = dsubmx (row_perm (lift_perm 0 k 1%g) M : 'M[F]_(1 + m, n)).
proof: Proof. by apply/matrixP=> i j; rewrite !mxE rshift1 lift_perm_lift perm1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(ssralg fintype fingroup perm) mathcomp(matrix bigop zmodp mxalgebra) gauss