diff options
author | jadep <jade.philipoom@gmail.com> | 2016-06-13 14:59:17 -0400 |
---|---|---|
committer | jadep <jade.philipoom@gmail.com> | 2016-06-13 14:59:17 -0400 |
commit | a86f8004a280dcf5cb5c2ad15b902d63119430bb (patch) | |
tree | 9f1a86fc6a8f604fc14de0ed3e5acb106f10e5f1 /src/Util/NatUtil.v | |
parent | a37eb79f7750a419346211abb58ec45b79975da0 (diff) |
progress on second stage (conditional constant-time subtraction) of canonicalization proofs
Diffstat (limited to 'src/Util/NatUtil.v')
-rw-r--r-- | src/Util/NatUtil.v | 11 |
1 files changed, 11 insertions, 0 deletions
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). |