From 4cb63acdb7ea7e98d124274fec85d1a10d86d38d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 1 Jul 2016 09:12:41 -0700 Subject: Add tactic to split sums and differences in inequalities --- src/Util/ZUtil.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/Util/ZUtil.v') 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] ] -- cgit v1.2.3