Differential equation study: $y'=y^2-\frac{1}{1+x^2}$ I'd like to ask you how to write in a formal way my thoughts about this ODE study:
$$y'(x)=(y(x))^2-\frac{1}{1+x^2} \qquad y(0)=0$$
Let $y$ be the maximal solution of this Cauchy's problem.


*

*We notice that:
$$y \text{ is decreasing} \iff y < -\sqrt{\frac{1}{1+x^2}} \ \vee y> \sqrt{\frac{1}{1+x^2}}$$ and it's decreasing elsewhere. So, as we have $y(0)=0$, our solution is decreasing in the first place. I want to prove that there exists a $b \in (0,+\infty)$ such that after $b$ it starts to increase.
Suppose that our solution is always decreasing: then, by theorems on the monotonous functions, it has limit $l\in[-\infty,0)$ as $x \to +\infty$. But this is absurd as we have $\lim_{x\to \infty} \pm\sqrt{\frac{1}{1+x^2}}=0$ and so our solution must touch $g(x)=-\sqrt{\frac{1}{1+x^2}}$ in a point. But in this point the derivative $y'$ changes it sign and so the function must start to increase. By this it follows also that our solution is contained in $[-1,0]$ as $|g(x)|<1$.


First question: is it legit? Can I do it in a different and faster way?


*Clearly our solution can't have a breakdown as $y'(x)$ is always defined. So to prove that it has global existence we must prove that it doesn't have a blow-up. But this follows by saying that $g(x)$ is a super-solution:
$$g'(x)=0>y'(x) \ \forall x \in [0,+\infty)$$
I think that everything here is true but I am not sure about the formality of it.
The scheme of proof suggested by the exercise is this:


*

*Prove that firstly it's decreasing, then it starts to increase;

*Prove that it has global existence.

*Prove that $y(x) \in [-1,0] \ \forall x$
Can you show me how to fix this proof to make it rigorous please? Thanks in advance.
 A: My approach is a bit different, but it can probably be modified to fit into your scheme of proof.
For global existence of solution: Note that
\begin{align}
-\frac{1}{1+x^2}\leq y'(x)\leq y(x)^2\,.
\end{align}
The first inequality tells us that $y(x)\geq -\tan^{-1}(x)$. By Grönwall's inequality, $y'(x)\leq y(x)^2$ implies
\begin{align}
y(x)\leq y(a)\exp\left(\int_a^xy(s)\,ds\right)\,,
\end{align}
where $y$ is a local solution on some interval $[a,b]$. Since local solutions are bounded above and below, a global solution $y$ exists. Apply the inequality above with $a=0$, we get $y(x)\leq 0$ for all $x>0$.
Suppose, for contradiction, that $y$ is decreasing on $[a,+\infty)$ for some $a\geq 0$. Then $y'(x)\leq 0$ for all $x>a$, which implies $0\leq y(x)^2\leq\frac{1}{1+x^2}$. Since $\frac{1}{1+x^2}\to 0$ as $x\to+\infty$, by the squeeze law $y(x)\to 0$ as $x\to 0$. The only possibility is $y(x)=0$ for all $x>a$. But then $y(x)^2=\frac{1}{1+x^2}$, a contradiction.
Pick $a\geq 0$ such that $y'(a)\geq0$. Suppose, for contradiction, that $y$ is not monotone on $[a,+\infty)$. Pick $b>a$ such that $y'(b)<0$. Let $\alpha$ be the supremum of $\{x\in[a,b)\colon y'(x)=0\}$, which is non-empty. Since $y$ is not a decreasing function on $[b,+\infty)$, the sets $\{x>b\colon y'(x)=0\}$ is non-empty, and has an infimum $\beta$. By continuity of $y'$, we have $y'(\alpha)=y'(\beta)=0$, and $\beta>b>\alpha$. Hence
\begin{align}
y(\beta)=y(\alpha)+\int_\alpha^\beta y'(x)\,dx<y(\alpha)=-\sqrt{\frac{1}{1+\alpha^2}}<-\sqrt{\frac{1}{1+\beta^2}}=y(\beta)\,,
\end{align}
a contradiction. Therefore once $y$ stops decreasing, it never decreases anymore.
By our previous discussion, $y$ has a global minimum at some $a\geq0$. Then for any $x\geq 0$,
\begin{align}
y(x)\geq y(a)=-\sqrt{\frac{1}{1+a^2}}\geq -1.
\end{align}
We can actually improve it to get a strict inequality, because if $a=0$, then $y(a)=0>-1$. Hence the range of $y$ is contained in $(-1,0]$.
A: Another point-of-view for this Riccati equation is obtained using the parametrization $y=-\frac{u'}{u}$. Then the ODE transforms to the linear DE
$$
(1+x^2)u''(x)=u(x),~~~ u(0)=1,~u'(0)=0.
$$
As can easily be concluded, $u(x)$ and $u'(x)$ will stay positive and thus growing for $x>0$, so that $u(x)$ has no roots for $x>0$ and thus the solution $y(x)$ will exist for all $x>0$. 
Asymptotically, for large $x$, the equation is approximately $u''=0$, which has solutions $u(x)=Ax+B$, so that 
$$
y(x)\approx-\frac{A}{Ax+B}=\frac1{x+C}~\text{ for }~x\to\infty.
$$
