diff options
Diffstat (limited to 'theories/Zarith/auxiliary.v')
| -rw-r--r-- | theories/Zarith/auxiliary.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Zarith/auxiliary.v b/theories/Zarith/auxiliary.v index 0f0fbc52b..e7bcdcfab 100644 --- a/theories/Zarith/auxiliary.v +++ b/theories/Zarith/auxiliary.v @@ -388,7 +388,7 @@ Save. Lemma add_x_x : (x:positive) (add x x) = (xO x). Intros p; Apply convert_intro; Simpl; Rewrite convert_add; -Rewrite ZL6; Trivial with arith. +Unfold 3 convert ; Simpl; Rewrite ZL6; Trivial with arith. Save. Theorem Zcompare_Zmult_compatible : |