exhaustivity defined

[helm.git] / helm / software / matita / contribs / dama / dama_didactic / reals.ma

diff --git a/helm/software/matita/contribs/dama/dama_didactic/reals.ma b/helm/software/matita/contribs/dama/dama_didactic/reals.ma
index 7d8a068c8e4c48a3d09a7a38286802e789a73cf2..3328c0e962a83bc5ee929d38533d02d741744a1f 100644 (file)
--- a/helm/software/matita/contribs/dama/dama_didactic/reals.ma
+++ b/helm/software/matita/contribs/dama/dama_didactic/reals.ma
@@ -90,8 +90,8 @@ axiom Relev_le: ∀x,y:R.
 
 lemma stupido: ∀x:R.R0+x=x.
  assume x:R.
- conclude (R0+x) = (x+R0) by _.
-               = x by _
+ conclude (R0+x) = (x+R0).
+                 = x
  done.
 qed.