Add a tactic for making use of destructed <? in Z

1 files changed, 10 insertions, 0 deletions

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index c6686b63c..e0949c933 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -480,3 +480,13 @@ Proof.
   induction l; intros; try reflexivity.
   etransitivity; [ apply IHl | apply Z.le_max_r ].
 Qed.
+
+Ltac Zltb_to_Zlt :=
+  repeat match goal with
+         | [ H : (?x <? ?y) = ?b |- _ ]
+           => let H' := fresh in
+              rename H into H';
+              pose proof (Zlt_cases x y) as H;
+              rewrite H' in H;
+              clear H'
+         end.