[Agda] Two antagonistic definitions

[Pierre Lescanne (en)]

Here is my problem. I set it in the Vec data structure, since it is a 
well known.

Assume that I want to define both ++ and another operation ++ʳ


_++_ : ∀{A : Set}{n m : ℕ} → Vec A n → Vec A m → Vec A (n + m)
[] ++ v = v
(x ∷ v₁) ++ v₂ = x ∷ (v₁ ++ v₂)

_++ʳ_ : ∀{A : Set}{n m : ℕ} → Vec A n → Vec A m → Vec A (n + m)
v ++ʳ [] = v
v₁ ++ʳ (x ∷ v₂) = (v₁ ∷ʳ x) ++ʳ v₂

Agda does want to accept the second definition or the first if I use Vec 
A (m + n) instead.   How should I proceed ?

Pierre Lescanne