Corrected the example on the webpage (fixes #56)

1 files changed, 15 insertions, 11 deletions

diff --git a/README.md b/README.md
index 9983a1b..236ef2f 100644
--- a/README.md
+++ b/README.md
@@ -16,28 +16,32 @@ SMTCoq is distributed under the CeCILL-C license.
 Here is a very small example of the possibilities of SMTCoq: automatic proofs in group theory.
 
 ```coq
-Require Import SMTCoq.
+Require Import SMTCoq ZArith.
+
+Local Open Scope Z_scope.
 
 Section group.
-  Variable e : Z, inv : Z -> Z, op : Z -> Z -> Z.
+  Variable e : Z.
+  Variable inv : Z -> Z.
+  Variable op : Z -> Z -> Z.
 
   Hypothesis associative :
-    forall a b c, op a (op b c) = op (op a b) c.
-  Hypothesis identity : forall a, (op e a = a).
-  Hypothesis inverse : forall a, (op (inv a) a = e).
+    forall a b c, op a (op b c) =? op (op a b) c.
+  Hypothesis identity : forall a, (op e a =? a).
+  Hypothesis inverse : forall a, (op (inv a) a =? e).
 
   Add_lemmas associative identity inverse.
 
-  Lemma identity' :
-    forall a, (op a e = a).
-  Proof. smt. Qed.
-
   Lemma inverse' :
-    forall a, (op a (inv a) = e).
+    forall a : Z, (op a (inv a) =? e).
   Proof. smt. Qed.
 
+  Lemma identity' :
+    forall a : Z, (op a e =? a).
+  Proof. smt inverse'. Qed.
+
   Lemma unique_identity e':
-    (forall z, op e' z = z) -> e' = e.
+    (forall z, op e' z =? z) -> e' =? e.
   Proof. intros pe'; smt pe'. Qed.
 
   Clear_lemmas.