How to prove $\forall x,y\in\mathbb{R} : x^3+x^2y=y^2+xy \Leftrightarrow y=x^2\lor y=-x?$ Let $x,y\in\mathbb{R}$
Assume $x^3+x^2y=y^2+xy$ 
Then $x^2(x+y)=y(x+y)$
Then either $(x+y)=0$ or $(x+y)\ne0$
Assume $x+y=0$
Then $y=-x$
Assume $(x+y)\ne0$
Then $y=x^2$
Then $x^3+x^2y=y^2+xy \Rightarrow y=x^2\lor y=-x$
Now assume $y=x^2\lor y=-x$
Assume $y=x^2$
Then $(x+y)y=(x+y)x^2$ #By definition 
Then $xy+y^2=x^3+yx^2$
Then $x^3+x^2y=y^2+xy$
Assume $y=-x$
Then $y+x=0$ 
Also $x^2\times 0=y\times 0$ #By definition
Then $x^2(x+y)=y(x+y)$
Then $x^3+x^2y=y^2+xy$
Then $x^3+x^2y=y^2+xy \Leftarrow y=x^2\lor y=-x.$
Then $\forall x,y\in\mathbb{R} : x^3+x^2y=y^2+xy \Leftrightarrow y=x^2\lor y=-x.$
I am not sure if the proof is well structured. Could someone check?
 A: This is not feedback on your proof, but instead an alternative proof, which seems a lot shorter and simpler.$
\newcommand{\calc}{\begin{align} \quad &}
\newcommand{\op}[1]{\\ #1 \quad & \quad \unicode{x201c}}
\newcommand{\hints}[1]{\mbox{#1} \\ \quad & \quad \phantom{\unicode{x201c}} }
\newcommand{\hint}[1]{\mbox{#1} \unicode{x201d} \\ \quad & }
\newcommand{\endcalc}{\end{align}}
\newcommand{\ref}[1]{\text{(#1)}}
\newcommand{\equiv}{\Leftrightarrow}
\newcommand{\then}{\Rightarrow}
\newcommand{\when}{\Leftarrow}
\newcommand{\true}{\text{true}}
\newcommand{\false}{\text{false}}
$
Let's just calculate, for all real $\;x,y\;$:
$$\calc
    x^3+x^2y=y^2+xy
\op\equiv\hint{LHS: factor out common $\;x^2\;$; RHS: factor out common $\;y\;$}
    x^2(x+y) = y(y+x)
\op\equiv\hint{simplify: divide by $\;x+y\;$, avoiding division by zero}
    x^2 = y \;\lor\; x+y=0
\op\equiv\hint{arithmetic -- to achieve the stated goal}
    y = x^2 \;\lor\; y = -x
\endcalc$$
This completes the proof.
Note how this proves both directions at the same time, instead of having to do both $\;\then\;$ and $\;\when\;$.
It looks like you wanted to go more into detail for the middle step.  Is this perhaps because you were given a list of real number axioms that you must use?
