关于Engels《解题策略》中E1题不变性原理解法的细节补充问询

我正在啃Engels《解题策略》里的E1题，用不变性原理来解题。书里给了解答思路，但我感觉有些关键细节没讲透，下面我把书中的内容转述一下，想请教大家补充缺失的部分：

问题设定 #

初始点为 ( S = (a,b) )，满足 ( 0 < b < a )，通过以下递归规则生成序列：
$$
x_0 = a, \quad y_0 = b, \quad x_{n+1} = \frac{x_n + y_n}{2}, \quad y_{n+1} = \frac{2x_n y_n}{x_n + y_n}.
$$

书中给出的不变量推导 #

作者指出了一个核心不变量：
$$
x_{n+1} y_{n+1} = \left(\frac{x_n + y_n}{2} \right)\left(\frac{2x_n y_n}{x_n + y_n} \right)= x_n y_n.
$$
由此直接得出 ( x_1 y_1 = x_0 y_0 = ab )，再通过数学归纳法就能推出对所有非负整数 ( n )，都有 ( x_n y_n = ab )。

不过到这里，书中只提了一句“对每个 ( n ) 都有 ( y_n < x_n )”，但完全没讲这个结论的推导过程。我自己试着推了推，但总觉得逻辑不严谨，想请教一下这部分的完整推导细节，以及这个结论在整个解题过程里的作用是什么？

备注：内容来源于stack exchange，提问作者Cardinality