...

diff --git a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex
index 945740cf8adf06ca203469f0a5fc5a216994de6a..b79b81a7425c00c5181185eb54993a63b7b0b5fb 100644 (file)
--- a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex
+++ b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex
@@ -301,7 +301,7 @@ with the scalar.
 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