diff options
| -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. |