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