Эквивалентность поиска плоской матрицы и 2D-матрицы (доказательство) — стремление к большей элегантности

У меня есть доказательство (очевидного) утверждения о том, что поиск элементов в сплющенном представлении матрицы в виде вектора длины m * n совпадает с представлением вектора вектора. Но мое доказательство кажется неуклюжим. [Я не буду приводить доказательства этого здесь, так как это искажает результаты поиска!]. Чтобы сделать этот вопрос самодостаточным, ниже я привожу самодостаточный модуль Agda с несколькими полезными леммами. [Некоторые из этих лемм, вероятно, должны быть в стандартной библиотеке, но их нет.]

По сути, я ищу элегантный способ заполнить дыру внизу, доказательство lookup∘concat. Если вы также можете сделать мои леммы более элегантными, не стесняйтесь!

module NNN where

open import Data.Nat
open import Data.Nat.Properties.Simple
open import Data.Nat.Properties
open import Data.Vec
open import Data.Fin using (Fin; inject≤; fromℕ; toℕ)
open import Data.Fin.Properties using (bounded)
open import Data.Product using (_×_; _,_)
open import Relation.Binary.PropositionalEquality

-- some useful lemmas
cong+r≤ : ∀ {i j} → i ≤ j → (k : ℕ) → i + k ≤ j + k
cong+r≤ {0}     {j}     z≤n       k = n≤m+n j k
cong+r≤ {suc i} {0}     ()        k -- absurd
cong+r≤ {suc i} {suc j} (s≤s i≤j) k = s≤s (cong+r≤ {i} {j} i≤j k)

cong+l≤ : ∀ {i j} → i ≤ j → (k : ℕ) → k + i ≤ k + j
cong+l≤ {i} {j} i≤j k =
  begin (k + i
           ≡⟨ +-comm k i ⟩ 
         i + k
           ≤⟨ cong+r≤ i≤j k ⟩ 
         j + k
           ≡⟨ +-comm j k ⟩ 
         k + j ∎)
  where open ≤-Reasoning

cong*r≤ : ∀ {i j} → i ≤ j → (k : ℕ) → i * k ≤ j * k
cong*r≤ {0}     {j}     z≤n       k = z≤n
cong*r≤ {suc i} {0}     ()        k -- absurd
cong*r≤ {suc i} {suc j} (s≤s i≤j) k = cong+l≤ (cong*r≤ i≤j k) k 

sinj≤ : ∀ {i j} → suc i ≤ suc j → i ≤ j
sinj≤ {0}     {j}     _        = z≤n
sinj≤ {suc i} {0}     (s≤s ()) -- absurd
sinj≤ {suc i} {suc j} (s≤s p)  = p

i*n+k≤m*n : ∀ {m n} → (i : Fin m) → (k : Fin n) → 
            (suc (toℕ i * n + toℕ k) ≤ m * n)
i*n+k≤m*n {0} {_} () _
i*n+k≤m*n {_} {0} _ ()
i*n+k≤m*n {suc m} {suc n} i k = 
  begin (suc (toℕ i * suc n + toℕ k) 
           ≡⟨  cong suc (+-comm (toℕ i * suc n) (toℕ k))  ⟩
         suc (toℕ k + toℕ i * suc n)
           ≡⟨ refl ⟩
         suc (toℕ k) + (toℕ i * suc n)
           ≤⟨ cong+r≤ (bounded k) (toℕ i * suc n) ⟩ 
         suc n + (toℕ i * suc n)
           ≤⟨ cong+l≤ (cong*r≤ (sinj≤ (bounded i)) (suc n)) (suc n) ⟩
         suc n + (m * suc n) 
           ≡⟨ refl ⟩
         suc m * suc n ∎)
  where open ≤-Reasoning

fwd : {m n : ℕ} → (Fin m × Fin n) → Fin (m * n)
fwd {m} {n} (i , k) = inject≤ (fromℕ (toℕ i * n + toℕ k)) (i*n+k≤m*n i k)

lookup∘concat : ∀ {m n} {A : Set} (i : Fin m) (j : Fin n) 
  (xss : Vec (Vec A n) m) → 
  lookup (fwd (i , j)) (concat xss) ≡ lookup j (lookup i xss)
lookup∘concat i j xss = {!!}