各位大佬好，我现在卡在一个微分方程组的单调性证明问题上，想请大家帮忙看看！

问题背景 #

我有两个微分方程组：
系统(1)：
$$
\begin{cases}
S_1’=-bS_1I_1+(1-c)aI_1 \
I_1’=bS_1I_1-aI_1
\end{cases}
$$
系统(2)：
$$
\begin{cases}
S_2’=-bS_2I_2+aI_2 \
I_2’=bS_2I_2-aI_2
\end{cases}
$$
所有参数满足 $a,b,c>0$，且两个系统有相同的初始条件：$S_1(0)=S_2(0)=s_0>0$，$I_1(0)=I_2(0)=i_0>0$。

我想要证明的结论是：当 $s_0>\frac{a}{b}$ 时，$S_1-S_2$ 是单调递减的函数。

目前已完成的推导 #

• 已经证明：对于所有 $t>0$，$S_1-S_2<0$ 且 $I_1-I_2<0$；
• 求出了 $S_1$ 和 $S_2$ 的解析表达式：
  $$
  S_1= \frac{(1-c)a}{b}+\left(s_0- \frac{(1-c)a}{b}\right)e^{-\int_{0}{t} bI_1(\tau) \ d\tau}
  $$
  $$
  S_2= \frac{a}{b}+\left(s_0- \frac{a}{b}\right)e^{-\int_{0}{t} bI_2(\tau) \ d\tau}
  $$
• 由上述表达式可得出：$S_1,S_2$ 均为单调递减函数；当 $s_0>\frac{a}{b}$ 时，$\frac{-ca}{b}<S_1-S_2<0$；
• 初始时刻满足 $(S_1-S_2)’<0$，且因为 $S_1,S_2$ 都是 $C^\infty$ 函数，$S_1-S_2$ 在初始阶段是递减的；同时有 $\lim_{t\rightarrow \infty}(S_1-S_2)’(t)=0$；
• 我将 $(S_1-S_2)’$ 整理为 $(S_1-S_2)’=F(t)(S_1-S_2)+G(t)$ 的形式，其中 $G(t)$ 始终为负，$F(t)$ 要么全程为负，要么在某个时刻 $t_0$ 之后开始变负，且两者都会收敛到有限极限值。

遇到的困惑 #

尽管做了这些推导，我还是没法证明 $S_1-S_2$ 在所有 $t>0$ 时都是单调递减的。我通过数值模拟验证了这个结论确实成立，但尝试用反证法推导时一直找不到矛盾点，卡在这儿了，希望能得到大家的思路和帮助！

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