diff --git a/theories/base.v b/theories/base.v
index fd49fb6e283d13956a0e75a9e752f5d0d42741fa..a3aaf5282583cb08f2ec42b35eba745895b05fd4 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 e59828b9e3f34426c691cceb3d99f0c97a70242e..1313fc10cfeae3c77f767727e049ce540290b972 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 264f7ee346c8a61a82f92a71c25b4690a42d8de6..0681b7fd340e5cde9fde3b7ff5c21ad07f7613c5 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.