How to find the loop invariant in hoare triples
First understand the meaning of the loop invariant. It means a condition which is true in every iteration of the program/algorithm at the begining as well as at the termination of the loop. Your program is something like this.

$$ x &gt; 1 \text{ and } y &gt;1 $$

$$\text{ While } x &gt;0  $$

$$\hspace{4cm}\text{ Do } x:= x - 1, y:=y+2$$

$$\text{ End }$$

$$x + y &gt; 5$$

$2x+y &gt;5$ is an invariant as you described. It is visible from the program that both $x$ and $y$ will be greater than $1$ during the first iterataion of the loop. So in the first iteration of while loop $2x+y &gt; 5$(you can prove it). Notice in each iteration of the while loop the value of the $x$ gets decrease by value $1$ and value of y is getting increase by two so inequality $2x+ y  &gt;5$ will be satisfied. You can prove it. Now come to the termination condition, at this point $x$ will be a negative number and my claim is value of $y$ is going to be at least $5$. Thus the invariant $2x+y &gt; 5$ si true throught the iteration of the while loop.

Example : 

Let $x=2$ and $y=2$, then $2 \times 2+2 = 6 &gt; 5$ is satisfied. Now in the second iteration  $x = 1, y=4$ so $1 \times 2+4 &gt; 5$ satisfied. Now $x = 0, y = 6$, loop terminated, $2 \times 0+6 &gt; 5$.