Minimize $|a-1|^3+|b-1|^3$ with constant product $ab=s$ Let $0<s$, and define 
$$ F(s):=\min_{a,b \in \mathbb{R}^+,ab=s} \left(|a-1|^3+|b-1|^3\right). $$
I would like to find proofs for the claim
$$
F(s)=\begin{cases}
1 - 3 s - 2s^{3/2}=F\big(a(s),b(s)\big), &\text{ if } 0<s\le1/9, \\
2 + 6 s - 2(3 + s)s^{1/2}=F(\sqrt s,\sqrt s) &\text{ if } 1/9\le s<1,
\end{cases}
$$
where $a(s),b(s)$ are uniquely defined by the equation $a+b=1-\sqrt{s},ab=s$.
(Actually I am more interested in the exact value of $F(s)$, and less in the minima points themselves, but I thought that this additional information might be helpful to find other proofs as well). 

I have a proof which I present below, but I wonder if there is an easier way to prove this. 

Also, is there a math software that can solve such a problem? (I am rather ignorant on that stuff, unfortunately).
Edit:
I think that maybe one can prove this without differentiation, but I am not sure. The idea is to rewrite the symmetric polynomial $(a-1)^3+(b-1)^3$, as a polynomial in $a+b,ab$, and proceed from there, but I am not sure it really works.
My proof:
First, suppose that $s \le 1$. Then the minimum is obtained at a point $(a,b)$ where both $a,b$ are not greater than $1$. Indeed, if $a>1$ (and so $b <s \le 1$), we can replace $a$ by $1$ and $b$ by $s$ to get the same product, but now both numbers are closer to $1$ then before. In fact, a symmetric argument shows that if $s \ge 1$, then both $a,b \ge 1$.
In any case, the signs of $a-1,b-1$ are identical.
Expressing the constraint as $g(a,b)=ab-s=0$, and using Lagrange's multipliers, there exist a $\lambda$ such that
$$
(a-1)^2=\lambda b, (b-1)^2=\lambda a.
\tag{1}$$
(Here we used the assumption the fact that the signs of $a-1,b-1$ are identical).
Subtracting these equations, we get
$$
(a-b)(a+b-2)=-\lambda(a-b).
$$
So, one candidate is $a=b=\sqrt{s}$. If $a \neq b$, then 
$$
a+b=2-\lambda, ab =s \tag{2}.
$$
Thus, $a,b$ are the solutions of the quadratic 
$$ x^2+(\lambda-2)x+s=0$$ 
Say that $a \le b$. Then
$$ a=\frac{2-\lambda-\sqrt{c}}{2}, b=\frac{2-\lambda+\sqrt{c}}{2}, \, \, \, \text{where } \, \, c=(2-\lambda)^2-4s.$$
Plugging this into $(a-1)^2=\lambda b$ from equation $(1)$, we get
$$
(\lambda+\sqrt c)^2=\lambda (4-2\lambda+2\sqrt c),
$$
which simplifies into
$$ 3\lambda^2-4\lambda=-c=4s-(2-\lambda)^2.$$
Further simplification gives
$$ (\lambda-1)^2=s \Rightarrow 1-\lambda=\pm \sqrt s.$$
Thus, by equation $(2)$, $a+b=1\pm \sqrt s$. 
Comment: We can immediately see that this cannot happen when $s>1$. Applying the AM-GM inequality for $a,b$ implies that 
$$ a+b=1+\sqrt s \Rightarrow s \le 1, \,\,\,a+b=1-\sqrt s \Rightarrow  s \le \frac{1}{9}$$
Now, if $a+b=1 + \sqrt s$, the it is easy to deduce that $b \ge 1$. (recall we assumed before that $a \le b$). As commented at the beginning, the optimum point must be obtained where $a,b$ are both not greater than $1$. So, the only possible option is $b=1$, and then $a=\sqrt s$, which implies $s=ab=\sqrt s$ so $s=1$ and $F(1)=0$, $a=b=1$.
Thus, we are left with the option $a+b=1-\sqrt{s}$.
Solving explicitly the quadratic given by $a+b=1-\sqrt{s},ab=s$, we get explicit expressions $a(s),b(s)$. Then direct calculation gives
$$ F\big(a(s),b(s)\big)=1 - 3 s - 2s^{3/2}.$$
The quadratic for $a(s),b(s)$ is 
$$ x^2-(1-\sqrt s)x+s=0. \tag{3}$$
It has real solutions exactly when $(1-\sqrt s)^2 \ge 4s$, or (since $s>0$), $\sqrt s \le \frac{1}{3}$. (Equivalently, this can be seen from the AM-GM inequality for $a,b$ as above.)
Now,
$F(\sqrt s,\sqrt s)=2 + 6 s - 2(3 + s)s^{1/2}$, and all is left to do is to verify that 
$$ F(a(s),b(s)) \le F(\sqrt s,\sqrt s),$$ in the regime $s \le \frac{1}{9}$, where $a(s),b(s)$ exist, as solutions to the quadratic $(3)$.
Direct computation shows that
$$ F(\sqrt s,\sqrt s)-F(a(s),b(s))=(1-3\sqrt s)^2 \ge 0$$
(and equality happens only at $s=\frac{1}{9}$).
This finishes the proof.
 A: Since you have established that the signs of $a - 1$ and $b - 1$ are identical, one approach would be to find the extrema of $(a - 1)^3 + (b-1)^3$ and then remove those where $a - 1$ and $b - 1$ are of opposite signs.
Plugging in $b = {s \over a}$ directly, you are finding an extremum of the expression
$$f(a) = (a - 1)^3 + ({s \over a} - 1)^3$$
So the goal becomes to find a $a$ for which $f'(a) = 0$. If you do the algebra, $f'(a) = 0$ at some $a$ satisfying
$$(a - \sqrt{s})(a^2 + (\sqrt{s} - 1)a + s) = 0$$
So you have two possibilities, either $a = b = \sqrt{s}$, or $a$ and $b$ are the two roots of the quadratic equation $x^2 + (\sqrt{s} - 1)x + s = 0$. You can then plug these two possibilities into the expression $(a - 1)^3 + (b - 1)^3 $ to compare the two situations.
While this may look unpleasant to do, since $(a - 1)^3 + (b - 1)^3$ is a symmetric polynomial $(a^3 + b^3) - 3(a^2 + b^2) + 3(a + b) - 1$, you will end out getting a polynomial in $\sqrt{s}$ using $a + b = 1 - \sqrt{s}$ and $ab = s$. You seem to have already computed it to be $1 - 3s - 2s^{3 \over 2}$.
A: For $0 < s < 1$, we have
\begin{align}
F(s) &= \min_{a, b > 0;\ ab = s}\ |a-1|^3 + |b-1|^3 \\
&= \min_{a\ge b > 0;\ ab = s}\ |a-1|^3 + |b-1|^3\tag{1}\\
&= \min_{0 < b \le \sqrt{s}}\ \left|\frac{s}{b} - 1\right|^3 + (1-b)^3\\
&= \min_{s \le b \le \sqrt{s}}\ \left(1 - \frac{s}{b}\right)^3 + (1-b)^3. \tag{2}
\end{align}
Explanation: (1) holds due to symmetry.
(2) holds since $|\frac{s}{b} - 1|^3 + (1-b)^3$ is strictly decreasing on $0 < b \le s$,
and hence the minimizer occurs on the interval $s \le b \le \sqrt{s}$.
Let us solve (2).
The minimum may be achieved at points on $(s, \sqrt{s})$ with zero derivative,
or at the interval endpoints $s, \sqrt{s}$.
Let $g(b) = (1 - \frac{s}{b})^3 + (1-b)^3$.
We have $g(s) = (1-s)^3$ and $g(\sqrt{s}) = 2(1-\sqrt{s})^3$. We have
$$g'(b) = \frac{3s}{b^2}\Big(1 - \frac{s}{b}\Big)^2 - 3(1-b)^2.$$
Thus, we have, for $s < b < \sqrt{s}$,
\begin{align}
g'(b) = 0 \quad &\Longleftrightarrow  \quad \frac{\sqrt{s}}{b}\Big(1 - \frac{s}{b}\Big) = 1-b\\
&\Longleftrightarrow \quad (b - \sqrt{s})(b^2 - (1-\sqrt{s})b + s) = 0, \\
&\Longleftrightarrow \quad b^2 - (1-\sqrt{s})b + s = 0. \tag{3}
\end{align}
We split into two cases:
1) $0 < s < \frac{1}{9}$: The equation (3) has exactly one real root on $(s, \sqrt{s})$, i.e.,
$b_1 = \frac{1-\sqrt{s}}{2} - \frac{1}{2}\sqrt{-3s-2\sqrt{s} + 1}$.
We have (some details are given later)
$$g(b_1) = 1 - 3s - 2s^{3/2}. \tag{4}$$ 
It is easy to prove that $g(b_1) \le g(s) $ and $g(b_1)\le g(\sqrt{s})$.
Thus, $F(s) = g(b_1) = 1 - 3s - 2s^{3/2}$.
2) $\frac{1}{9} \le s < 1$: The equation (3) has no real root on $(s, \sqrt{s})$.
Thus, $F(s) = \min(g(s), g(\sqrt{s})) = g(\sqrt{s}) = 2 - 6\sqrt{s} + 6s - 2s^{3/2}$.
We are done.
$\phantom{2}$
Some details about (4):
From $b_1^2 - (1-\sqrt{s})b_1 + s = 0$, we have
$s = (1-\sqrt{s})b_1 - b_1^2$ and $\frac{s}{b_1} = 1-\sqrt{s} - b_1$.
Thus, 
\begin{align}
g(b_1) &= (1 - \frac{s}{b_1})^3 + (1-b_1)^3 \\
&= (\sqrt{s} + b_1)^3 + (1-b_1)^3\\
&= (3\sqrt{s}+3)b_1^2 - (3-3s)b_1 + s^{3/2} + 1\\
&= 3(1+\sqrt{s})[b_1^2 - (1-\sqrt{s})b_1] + s^{3/2} + 1\\
&= 3(1+\sqrt{s})\cdot (-s) + s^{3/2} + 1\\
&= 1 - 3s - 2 s^{3/2}.
\end{align}
