diff --git a/prelude/collections.v b/prelude/collections.v
index afe28a10cd45c4f97003abb17b44e576dc474060..b0e0cb54c2c97f356cf57fbedf6a4192c4065881 100644
--- a/prelude/collections.v
+++ b/prelude/collections.v
@@ -531,12 +531,21 @@ End fresh.
 Section collection_monad.
   Context `{CollectionMonad M}.
 
+  Global Instance collection_fmap_mono {A B} :
+    Proper (pointwise_relation _ (=) ==> (⊆) ==> (⊆)) (@fmap M _ A B).
+  Proof. intros f g ? X Y ?; solve_elem_of. Qed.
   Global Instance collection_fmap_proper {A B} :
     Proper (pointwise_relation _ (=) ==> (≡) ==> (≡)) (@fmap M _ A B).
   Proof. intros f g ? X Y [??]; split; solve_elem_of. Qed.
+  Global Instance collection_bind_mono {A B} :
+    Proper (((=) ==> (⊆)) ==> (⊆) ==> (⊆)) (@mbind M _ A B).
+  Proof. unfold respectful; intros f g Hfg X Y ?; solve_elem_of. Qed.
   Global Instance collection_bind_proper {A B} :
     Proper (((=) ==> (≡)) ==> (≡) ==> (≡)) (@mbind M _ A B).
   Proof. unfold respectful; intros f g Hfg X Y [??]; split; solve_elem_of. Qed.
+  Global Instance collection_join_mono {A} :
+    Proper ((⊆) ==> (⊆)) (@mjoin M _ A).
+  Proof. intros X Y ?; solve_elem_of. Qed.
   Global Instance collection_join_proper {A} :
     Proper ((≡) ==> (≡)) (@mjoin M _ A).
   Proof. intros X Y [??]; split; solve_elem_of. Qed.
diff --git a/prelude/sets.v b/prelude/sets.v
index ada3a408add66ba944c0b9e9fcc541ba60e80e91..e92b14e6f635e8bec8fc5f4d043f01bc6a756616 100644
--- a/prelude/sets.v
+++ b/prelude/sets.v
@@ -28,4 +28,4 @@ Instance set_join : MJoin set := λ A (XX : set (set A)),
 Instance set_collection_monad : CollectionMonad set.
 Proof. by split; try apply _. Qed.
 
-Global Opaque set_union set_intersection.
+Global Opaque set_union set_intersection set_difference.