Как да разрешите тази грешка в agda?

Дефинирах Поток от положително рационално по този начин.

one : ℤ
one = + 1

--giving a rational as input it will return next rational (in some down tailing method)
next : pair → pair
next q = if (n eq one) then (mkPair (+ m Data.Integer.+ one) 1)
         else (mkPair (n Data.Integer.- one) (m Nat.+ 1))
  where
     n = getX q
     m = getY q

--it will generate all rational from (1,1)
rational : Stream pair
rational = iterate next (mkPair one 1) 

--it will get all the rational which are greater than the given rational. 
RQ : pair → Stream pair → Stream pair
RQ q (x ∷ xs) = (x add q) ∷ ♯ (RQ q (♭ xs))    

--This is a stream of positive rational greater than (0,1).
positiveRat : Stream pair
positiveRat = RQ (mkPair (+ 0) (1)) rational

тук двойка е запис с две полета Z и N.

Сега искам да докажа, че „за всички x, ако x > 0, тогава x ще принадлежи към Поток от положително рационално.

 open import Data.Stream
 open import Data.Nat
 open import Data.Rational
 open import Data.Integer
 open import Coinduction

lemma : (x : pair) → ((+ 0) Data.Integer.≤ (pair.x x)) → ( x ∈ positiveRat ) 
lemma q proof = ?

Опит за разделяне на доказателство води до следното съобщение за грешка:

 I'm not sure if there should be a case for the constructor +≤+,
because I get stuck when trying to solve the following unification
problems (inferred index ≟ expected index):
  + m ≟ + 0
  + n ≟ getX q₁
when checking that the expression ? has type q ∈ positiveRat

Моля, помогнете за разрешаването на тази грешка.