Just a little hint: I think you should enforce that your list (list A) actually represents an m x n matrix. First, you could define a function isMatrix (A : matrix) (m n : nat) : bool (e.g. using List.Forall and List.length).Then define a function get (A : matrix) (i j : nat) : option A (e.g. using List.nth_error) and show that it always returns a value if the indexes are ‘in range’. You could try to proof that if you have a m x n matrix, inverting it makes an n x m matrix. Prove that two matrixes are equal if and only if they contain the same elements, using the function get for all in-range coordinates. Finally, the crutial property for transpose is that get (transpose M) m n = get M n m (if n, m are in-range).
(I always forget whether n or m is the number of columns / rows, but this is up to you to define.)
An alternative approach is to use Vector.t, which is a list of fixed length (see my last post). Unfortunately, using this depdent data type can be a bit complicated for beginners, because the standard library lacks a lot of useful definitions and lemmas.