From a86f8004a280dcf5cb5c2ad15b902d63119430bb Mon Sep 17 00:00:00 2001
From: jadep <jade.philipoom@gmail.com>
Date: Mon, 13 Jun 2016 14:59:17 -0400
Subject: progress on second stage (conditional constant-time subtraction) of
 canonicalization proofs

---
 src/Util/NatUtil.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'src/Util/NatUtil.v')

diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v
index 1f69b04d2..59898be7a 100644
--- a/src/Util/NatUtil.v
+++ b/src/Util/NatUtil.v
@@ -57,7 +57,18 @@ Proof.
   }
 Qed.
 
+Lemma lt_min_l : forall x a b, (x < min a b)%nat -> (x < a)%nat.
+Proof.
+  intros ? ? ? lt_min.
+  apply Nat.min_glb_lt_iff in lt_min.
+  destruct lt_min; assumption.
+Qed.
 
+(* useful for hints *)
+Lemma eq_le_incl_rev : forall a b, a = b -> b <= a.
+Proof.
+  intros; omega.
+Qed.
 
 Lemma beq_nat_eq_nat_dec {R} (x y : nat) (a b : R)
   : (if EqNat.beq_nat x y then a else b) = (if eq_nat_dec x y then a else b).
-- 
cgit v1.2.3