Finding a good loop invariant

Question

I want to prove that the following program is correct. The code takes an array i of length N and a number x. At the end, the value of found should be true if the array contains x and false otherwise.

found := false;
i := 0 ;
while i < N do {
    found := found || (a[i]=x);
    i:=i+1
}

The given preconditions are that N >= 0 and that the array is sorted in ascending order (however, I don't know how the fact that it is sorted can help).

As postcondition, I think the following would suffice: the value of found equals the value of the predicate “there exists an i in the range [0, N) such that a[i] == x”

However, I am stuck at this point and don't know how to continue. I cannot think of any loop invariant that has any relation to the postcondition. What would you suggest as a loop invariant?