\end{displaymath}
\end{exercise}
-\myincludegraphics{step1}{t}{12cm}{Example session, snapshot 1.}
- {Example session, snapshot 1.}
+\myincludegraphics{step1}{t}{12cm}{Example session.}
+ {Example session.}
%\myincludegraphics{step2}{t}{4cm}{Example session, snapshot 2.}
% {Example session, snapshot 2.}
The user proceeds by istantiating the scalar with the number 2. The
\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*\frac{((x+1)*(x+1)-1-x*x)}{2}$.
+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
expression using the lemma $Rinv\_r\_simpl\_m$ that states that
$\forall x,y.\;y = x * y * x^{-1}$. Since we do not provide yet any tutor