Hola.
Una matriz escalonada no tiene todos los elementos para la dimensión n*n. La primera columna contiene un sólo elemento, la segunda columna 2 elementos, la tercera 3 y así sucesivamente, de tal manera que la columna n posee n elementos. Gráficamente podría verse algo así como:
X X X ... X
X X ... X
X ... X
... X
El operador addM podría expresar que dada una matriz escalonada de n columnas y un arreglo de n+1 elementos, se genera una matriz escalonada de n+1 columnas (construyendo de abajo hacia arriba para la gráfica previa):
Parameter addM : forall (X : Set) (n : nat), Matrix X n -> Array X (n+1) -> Matrix X (n+1).
Saludos, Carlos