Remove the mod on eval_add

1 files changed, 2 insertions, 3 deletions

diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v
index ed96850cb..1dc466849 100644
--- a/src/Experiments/SimplyTypedArithmetic.v
+++ b/src/Experiments/SimplyTypedArithmetic.v
@@ -228,9 +228,8 @@ Module Positional. Section Positional.
          from_associational n (a_a ++ b_a).
     Lemma eval_add n (f g:list Z)
           (Hf : length f = n) (Hg : length g = n) :
-      eval n (add n f g) mod m = (eval n f + eval n g) mod m.
-    Proof. cbv [add]; rewrite Hm in *; push; trivial.
-    destruct n; auto.                                         Qed.
+      eval n (add n f g) = (eval n f + eval n g).
+    Proof. cbv [add]; push; trivial. destruct n; auto.        Qed.
   End add.
 
   Section sub.