Reversing a Vec in Lean 4

Vec.lean

inductive Vec (α : Type u) : Nat → Type u where
| nil : Vec α 0
| cons : α → Vec α n → Vec α (n + 1)
deriving Repr

def Vec.reverse {α : Type u} {n : Nat} (xs : Vec α n) : Vec α n := loop xs nil
where
  loop {n m : Nat} : Vec α n → Vec α m → Vec α (n + m)
  | nil, acc => by rwa [Nat.zero_add]
  | @cons _ n x xs, acc => by
    have := loop xs (cons x acc)
    rwa [Nat.add_comm, Nat.add_left_comm]