diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-09-14 14:09:29 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-09-14 14:09:29 -0400 |
| commit | 1ecf2f9945a99b5e4a58ebe46ec5764f07ec05aa (patch) | |
| tree | 9aff24c029e54f6a55ae5178ea99b3ab68513735 /src/Util/ZUtil.v | |
| parent | 6ae005c290f557a9a719792909edb93311f07dd5 (diff) | |
More 8.4 compatibility
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index abae9de41..ce473fcb4 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -1681,7 +1681,8 @@ Module Z. Lemma lt_mul_2_mod_sub : forall a b, b <> 0 -> b <= a < 2 * b -> a mod b = a - b. Proof. - intros; replace a with (1 * b + (a - b)) at 1 by ring. + intros. + replace (a mod b) with ((1 * b + (a - b)) mod b) by (f_equal; ring). rewrite Z.mod_add_l by auto. apply Z.mod_small. omega. |