From dbbda8cb715b5fb4f626a26b1aa76ba616aae3be Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 26 Aug 2014 00:21:37 +0200
Subject: [PATCH] =?UTF-8?q?Prove=20that=20lockset=20=E2=8A=86=20dom=20memo?=
 =?UTF-8?q?ry.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/base.v        | 4 ++++
 theories/collections.v | 4 ++++
 theories/numbers.v     | 6 +++++-
 3 files changed, 13 insertions(+), 1 deletion(-)

diff --git a/theories/base.v b/theories/base.v
index fd49fb6e..a3aaf528 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -815,6 +815,10 @@ Section prod_relation.
 End prod_relation.
 
 (** ** Other *)
+Lemma and_wlog_l (P Q : Prop) : (Q → P) → Q → (P ∧ Q).
+Proof. tauto. Qed.
+Lemma and_wlog_r (P Q : Prop) : P → (P → Q) → (P ∧ Q).
+Proof. tauto. Qed.
 Instance: ∀ A B (x : B), Commutative (=) (λ _ _ : A, x).
 Proof. red. trivial. Qed.
 Instance: ∀ A (x : A), Associative (=) (λ _ _ : A, x).
diff --git a/theories/collections.v b/theories/collections.v
index e59828b9..1313fc10 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -35,6 +35,10 @@ Section simple_collection.
   Qed.
   Lemma collection_positive_l_alt X Y : X ≢ ∅ → X ∪ Y ≢ ∅.
   Proof. eauto using collection_positive_l. Qed.
+  Lemma elem_of_singleton_1 x y : x ∈ {[y]} → x = y.
+  Proof. by rewrite elem_of_singleton. Qed.
+  Lemma elem_of_singleton_2 x y : x = y → x ∈ {[y]}.
+  Proof. by rewrite elem_of_singleton. Qed.
   Lemma elem_of_subseteq_singleton x X : x ∈ X ↔ {[ x ]} ⊆ X.
   Proof.
     split.
diff --git a/theories/numbers.v b/theories/numbers.v
index 264f7ee3..0681b7fd 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -264,7 +264,11 @@ Arguments Z.modulo _ _ : simpl never.
 Arguments Z.quot _ _ : simpl never.
 Arguments Z.rem _ _ : simpl never.
 
-Lemma Z_mod_pos a b : 0 < b → 0 ≤ a `mod` b.
+Lemma Z_to_nat_neq_0_pos x : Z.to_nat x ≠ 0%nat → 0 < x.
+Proof. by destruct x. Qed.
+Lemma Z_to_nat_neq_0_nonneg x : Z.to_nat x ≠ 0%nat → 0 ≤ x.
+Proof. by destruct x. Qed.
+Lemma Z_mod_pos x y : 0 < y → 0 ≤ x `mod` y.
 Proof. apply Z.mod_pos_bound. Qed.
 
 Hint Resolve Z.lt_le_incl : zpos.
-- 
GitLab