Properties of preference relation
If we define $\succeq$ on $X$ as the primitive, then the strict preference relation is derived as
$$ x\succ y ~\Leftrightarrow~ x\succeq y ~\text{ but not }~ y\succeq x.$$

Note that you can view this as a definition of $\succ$. Now we prove $y\succeq x$ iff not $x\succ y$:

$(\Rightarrow)$ If $y\succeq x$, by definition, $x\succ y$ is not true;

$(\Leftarrow)$ If not $x\succ y$, then there are only three possibilities: (i) $ x\succeq y$ and $y\succeq x$; (ii) not $x\succeq y$ but $y\succeq x$; and (iii) neither $x\succeq y$ nor $y\succeq x$. Case (iii) can be ruled out if we assume completeness of $\succeq$. Therefore, in both (i) and (ii), we have $y\succeq x$.

It's worth mentioning that Kreps (1990) introduces another approach to define preference relations on $X$. He takes $\succ$ as the primitive and then derives the weak preference relation as:
$$x\succeq y ~\Leftrightarrow~ \text{not }~ y\succ x.$$

In this case, there is no need to prove the equivalence since it is a definition.