From 69fc6dabced75fd38eaf89c4186d7de0ccff93b8 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Fri, 14 Apr 2017 20:45:24 -0400
Subject: Add base_type_leb_total

---
 src/Compilers/Z/Syntax/Util.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/Compilers/Z/Syntax/Util.v b/src/Compilers/Z/Syntax/Util.v
index 26803e851..9f18f47e9 100644
--- a/src/Compilers/Z/Syntax/Util.v
+++ b/src/Compilers/Z/Syntax/Util.v
@@ -270,3 +270,10 @@ Lemma cast_back_flat_const_prod {var A B f} {V : _ * _}
     = (@cast_back_flat_const var A f (fst V) (fst v),
        @cast_back_flat_const var B f (snd V) (snd v)).
 Proof. reflexivity. Qed.
+
+Lemma base_type_leb_total
+  : forall x y : base_type, base_type_leb x y = true \/ base_type_leb y x = true.
+Proof.
+  induction x, y; simpl; auto.
+  rewrite !Nat.leb_le; omega.
+Qed.
-- 
cgit v1.2.3