diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-01 09:12:41 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-01 09:12:41 -0700 |
| commit | 4cb63acdb7ea7e98d124274fec85d1a10d86d38d (patch) | |
| tree | 84ae1bab728966db9fd5be739d03dd74963fe945 /src/Util/ZUtil.v | |
| parent | bb37a1f7f16731b4a6d393fc113bdf5348a5ad78 (diff) | |
Add tactic to split sums and differences in inequalities
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 6d6039a6d..84d9ed3da 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -545,6 +545,8 @@ Ltac Zsplit_sums_step := | [ |- _ - _ <= _ ] => etransitivity; [ eapply Z.sub_le_mono | ] end. +Ltac Zsplit_sums := + try (Zsplit_sums_step; [ Zsplit_sums | ]). Ltac Zpre_reorder_fractions_step := match goal with | [ |- context[?x / ?y * ?z] ] |