-\texttt{Assumption} tutor now suggests to close the second goal by applying
-the hypothesis $H$. No useful suggestions, instead, are generated for the
-main goal $2x = 2*((x+1)*(x+1)-1-x*x)*2^{-1}$.
-To proceed in the proof, indeed, the user needs to symplify the
+\texttt{Assumption} tutor now suggests to close the second goal (that
+states that $2 \neq 0$) by applying the hypothesis $H$.
+No useful suggestions, instead, are generated for the main goal
+$2*x = 2*((x+1)*(x+1)-1-x*x)*2^{-1}$.
+To proceed in the proof the user needs to symplify the