diff options
Diffstat (limited to 'contrib/omega/Zcomplements.v')
| -rw-r--r-- | contrib/omega/Zcomplements.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/omega/Zcomplements.v b/contrib/omega/Zcomplements.v index 07da48230..c80823237 100644 --- a/contrib/omega/Zcomplements.v +++ b/contrib/omega/Zcomplements.v @@ -192,7 +192,7 @@ Induction a. Intro p; Simpl. Repeat Rewrite POS_xI. -Rewrite (POS_xO (xO (floor_pos p))). +Rewrite (POS_xO (xO (floor_pos p))). Rewrite (POS_xO (floor_pos p)). Omega. |