Ssreflect Users Discussion List

[Vincent Siles <>]

Hi everyone,

my final goal is to prove that
forall m n (I: 'rV[R]_m) (J: 'rV[R]_n), exists M, row_mx I J = (row_mx J I) 
*m M

I think the easiest way to prove this is to "translate" all columns of
row_mx I J to the
 right by n position, as in :  { 0 1 | 2 3 4} -> {2 3 4 | 0 1 }
With this, I should get to row_mx J I, so I guess that M is a
permutation matrix
(with a nice cast around it). My problem is that I can manage to
define this permutation.

Is there an easy way to define this translation permutation ?

Best,
Vincent