[proofplan]
We prove that every comparable pair in a finite poset is connected by a saturated chain of cover relations. The forward implication is proved by induction on the cardinality of the interval $[x,y]$. If $x<y$ is not itself a cover relation, we choose an intermediate element $z$ with $x<z<y$, apply the induction hypothesis on the smaller intervals $[x,z]$ and $[z,y]$, and concatenate the resulting cover chains. The reverse implication follows directly from the definition of the cover relation and transitivity of the partial order.
[/proofplan]
[step:Reduce the forward implication to induction on finite intervals]
For $a,b\in P$ with $a\le b$, define the interval
\begin{align*}
[a,b]:=\{p\in P:a\le p\le b\}.
\end{align*}
Since $P$ is finite, the interval $[a,b]$ is finite. We prove by induction on the integer $|[a,b]|$ the following assertion:
For every pair $a,b\in P$ with $a\le b$, either $a=b$, or there exist an integer $r\ge 1$ and elements $a_0,\dots,a_r\in P$ such that
\begin{align*}
a=a_0\lessdot a_1\lessdot \cdots \lessdot a_r=b.
\end{align*}
If $|[a,b]|=1$, then $[a,b]=\{a\}$, so $b=a$. Thus the assertion holds in the base case.
[/step]
[step:Split a non-cover comparison through an intermediate element]
Assume the induction assertion holds for all comparable pairs whose interval has cardinality less than $N$, and let $a,b\in P$ satisfy $a\le b$ and $|[a,b]|=N$.
If $a=b$, the assertion holds. Suppose $a<b$. If $a\lessdot b$, then taking $r=1$, $a_0=a$, and $a_1=b$ gives the required cover chain.
It remains to treat the case where $a<b$ and $a\not\lessdot b$. By the definition of the cover relation, there exists $z\in P$ such that
\begin{align*}
a<z<b.
\end{align*}
Then $[a,z]\subset [a,b]$ and $b\notin [a,z]$, so $|[a,z]|<|[a,b]|=N$. Also $[z,b]\subset [a,b]$ and $a\notin [z,b]$, so $|[z,b]|<N$.
By the induction hypothesis applied to $a\le z$, there exist an integer $r\ge 1$ and elements $a_0,\dots,a_r\in P$ such that
\begin{align*}
a=a_0\lessdot a_1\lessdot \cdots \lessdot a_r=z.
\end{align*}
By the induction hypothesis applied to $z\le b$, there exist an integer $s\ge 1$ and elements $b_0,\dots,b_s\in P$ such that
\begin{align*}
z=b_0\lessdot b_1\lessdot \cdots \lessdot b_s=b.
\end{align*}
Concatenating these two chains and omitting the repeated element $z=a_r=b_0$ gives
\begin{align*}
a=a_0\lessdot a_1\lessdot \cdots \lessdot a_r=b_0\lessdot b_1\lessdot \cdots \lessdot b_s=b.
\end{align*}
This is a finite sequence of cover relations from $a$ to $b$, completing the induction step.
[guided]
We want to show that whenever $a\le b$, the order relation from $a$ to $b$ can be recovered by walking upward through cover relations. The natural measure of complexity is the size of the interval
\begin{align*}
[a,b]:=\{p\in P:a\le p\le b\}.
\end{align*}
This is finite because $P$ is finite, so induction on $|[a,b]|$ is legitimate.
Assume the desired assertion is known for all comparable pairs whose intervals have cardinality less than $N$, and let $a,b\in P$ satisfy $a\le b$ and $|[a,b]|=N$. If $a=b$, there is no cover chain to build, and this is exactly the equality case allowed in the statement. Now suppose $a<b$. If $a\lessdot b$, then the one-step sequence
\begin{align*}
a=a_0\lessdot a_1=b
\end{align*}
has the required form.
The only remaining case is that $a<b$ but $a$ is not covered by $b$. By definition, $a\lessdot b$ means that $a<b$ and there is no element strictly between them. Since $a<b$ holds but $a\lessdot b$ does not, there must exist an element $z\in P$ such that
\begin{align*}
a<z<b.
\end{align*}
This element splits the interval from $a$ to $b$ into two smaller intervals. Indeed, $[a,z]\subset [a,b]$, and $b\notin [a,z]$ because $z<b$, so
\begin{align*}
|[a,z]|<|[a,b]|=N.
\end{align*}
Similarly, $[z,b]\subset [a,b]$, and $a\notin [z,b]$ because $a<z$, so
\begin{align*}
|[z,b]|<N.
\end{align*}
Now the induction hypothesis applies to both smaller comparable pairs $a\le z$ and $z\le b$. Applied to $a\le z$, it gives an integer $r\ge 1$ and elements $a_0,\dots,a_r\in P$ satisfying
\begin{align*}
a=a_0\lessdot a_1\lessdot \cdots \lessdot a_r=z.
\end{align*}
Applied to $z\le b$, it gives an integer $s\ge 1$ and elements $b_0,\dots,b_s\in P$ satisfying
\begin{align*}
z=b_0\lessdot b_1\lessdot \cdots \lessdot b_s=b.
\end{align*}
The endpoint of the first chain is the starting point of the second chain, namely $z=a_r=b_0$. Therefore we concatenate the two chains while writing $z$ only once:
\begin{align*}
a=a_0\lessdot a_1\lessdot \cdots \lessdot a_r=b_0\lessdot b_1\lessdot \cdots \lessdot b_s=b.
\end{align*}
Every adjacent relation displayed is still a cover relation in $P$, so this is the required cover chain from $a$ to $b$. This completes the induction step.
[/guided]
[/step]
[step:Apply the interval induction to obtain the forward implication]
Taking $a=x$ and $b=y$ in the induction assertion, if $x\le y$, then either $x=y$ or there exist an integer $m\ge 1$ and elements $x_0,\dots,x_m\in P$ such that
\begin{align*}
x=x_0\lessdot x_1\lessdot \cdots \lessdot x_m=y.
\end{align*}
This proves the forward implication.
[/step]
[step:Use transitivity to recover the order from a cover chain]
Conversely, suppose either $x=y$ or there exist an integer $m\ge 1$ and elements $x_0,\dots,x_m\in P$ such that
\begin{align*}
x=x_0\lessdot x_1\lessdot \cdots \lessdot x_m=y.
\end{align*}
If $x=y$, then $x\le y$ by reflexivity of the partial order. In the second case, each relation $x_i\lessdot x_{i+1}$ means $x_i<x_{i+1}$, hence $x_i\le x_{i+1}$, for every $i\in\{0,\dots,m-1\}$. Applying transitivity of $\le$ along this finite sequence gives
\begin{align*}
x=x_0\le x_1\le \cdots \le x_m=y.
\end{align*}
Thus $x\le y$. Combining this with the forward implication proves the equivalence.
[/step]
