diff options
| author |  Jason Gross <jagro@google.com> | 2016-06-30 17:55:12 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-06-30 17:55:27 -0700 |
| commit | 0e8adaa7c1e546f442ac7e0f6d3e81c0e7e985b8 (patch) | |
| tree | ffb5e73ab19db315a6af59e078607203cde5110d /src/Util/ZUtil.v | |
| parent | 4d9f63c4feab45d2f0701157fb21148dbb85ec0e (diff) | |
Add a proof of 2 * x - x = x
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 c20d59d20..ebfea8ebd 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -522,3 +522,6 @@ Proof. | [ x : Z |- _ ] => destruct x end ]. Qed. + +Lemma two_times_x_minus_x x : 2 * x - x = x. +Proof. lia. Qed. |