diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-17 14:56:40 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-17 14:56:40 -0400 |
| commit | 593093d4795fe497655f25ff26767d807e01bfea (patch) | |
| tree | 49bfbc7bf06ce0b8ccc8ffbcf3fdedfbae3d5e36 /src/Util/ZUtil.v | |
| parent | 2aba7f244a5a08af43481b1d06e81ec461fe58b7 (diff) | |
Add ZUtil lemma
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index d82896641..b61219480 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -2022,6 +2022,9 @@ Module Z. Proof. omega. Qed. Hint Rewrite simplify_2XmX : zsimplify. + Lemma simplify_add_pos x y : Z.pos x + Z.pos y = Z.pos (x + y). + Proof. reflexivity. Qed. + Lemma move_R_pX x y z : x + y = z -> x = z - y. Proof. omega. Qed. Lemma move_R_mX x y z : x - y = z -> x = z + y. |