diff options
Diffstat (limited to 'src/Experiments/SimplyTypedArithmetic.v')
| -rw-r--r-- | src/Experiments/SimplyTypedArithmetic.v | 5 |
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. |