diff --git a/CHANGELOG.md b/CHANGELOG.md
index 165438b0c84f65475349853d79bb90d708f71f4b..417c7c544a8b81c3d1af7e525442210e75203239 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -68,6 +68,9 @@ API-breaking change is listed.
 - Add lemmas `map_fold_union_strong`, `map_fold_union`,
   `map_fold_disj_union_strong`, `map_fold_disj_union` and `map_fold_proper`.
 - Add `gmultiset_map` and associated lemmas. (by Marijn van Wezel)
+- Add `CProd` type class for Cartesian products; with instances for `list`,
+  `gset`, `boolset`, `MonadSet` (i.e., `propset`, `listset`); and `set_solver`
+  tactic support. (by Thibaut Pérami)
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
diff --git a/stdpp/base.v b/stdpp/base.v
index 26fff8e206da17cb4a552bf1e09f482410e670c5..2a5741191b61b606cc6b8b5fa48a4e788049e583 100644
--- a/stdpp/base.v
+++ b/stdpp/base.v
@@ -1050,6 +1050,15 @@ Notation "(.∖ x )" := (λ y, difference y x) (only parsing) : stdpp_scope.
 Infix "∖*" := (zip_with (∖)) (at level 40, left associativity) : stdpp_scope.
 Notation "(∖*)" := (zip_with (∖)) (only parsing) : stdpp_scope.
 
+(** The operation [cprod X Y] gives the Cartesian product of set-like structures
+[X] and [Y], i.e., [cprod X Y := { (x,y) | x ∈ X, y ∈ Y }]. The implementation/
+instance depends on the representation of the set. *)
+Class CProd A B C := cprod : A → B → C.
+Global Hint Mode CProd ! ! - : typeclass_instances.
+Global Instance: Params (@cprod) 4 := {}.
+(** We do not have a notation for [cprod] (yet) since this operation seems
+not commonly enough used. *)
+
 Class Singleton A B := singleton: A → B.
 Global Hint Mode Singleton - ! : typeclass_instances.
 Global Instance: Params (@singleton) 3 := {}.
diff --git a/stdpp/boolset.v b/stdpp/boolset.v
index 5e1b5e1dd3e6fd1f79b2d4ebdfab4450d856fc5b..3e3d164d21e1bcbdae011b0b31a760348a6a5038 100644
--- a/stdpp/boolset.v
+++ b/stdpp/boolset.v
@@ -17,6 +17,10 @@ Global Instance boolset_intersection {A} : Intersection (boolset A) := λ X1 X2,
   BoolSet (λ x, boolset_car X1 x && boolset_car X2 x).
 Global Instance boolset_difference {A} : Difference (boolset A) := λ X1 X2,
   BoolSet (λ x, boolset_car X1 x && negb (boolset_car X2 x)).
+Global Instance boolset_cprod {A B} :
+  CProd (boolset A) (boolset B) (boolset (A * B)) := λ X1 X2,
+  BoolSet (λ x, boolset_car X1 x.1 && boolset_car X2 x.2).
+
 Global Instance boolset_top_set `{EqDecision A} : TopSet A (boolset A).
 Proof.
   split; [split; [split| |]|].
@@ -31,6 +35,19 @@ Qed.
 Global Instance boolset_elem_of_dec {A} : RelDecision (∈@{boolset A}).
 Proof. refine (λ x X, cast_if (decide (boolset_car X x))); done. Defined.
 
+Lemma elem_of_boolset_cprod {A B} (X1 : boolset A) (X2 : boolset B) (x : A * B) :
+  x ∈ cprod X1 X2 ↔ x.1 ∈ X1 ∧ x.2 ∈ X2.
+Proof. apply andb_True. Qed.
+
+Global Instance set_unfold_boolset_cprod {A B} (X1 : boolset A) (X2 : boolset B) x P Q :
+  SetUnfoldElemOf x.1 X1 P → SetUnfoldElemOf x.2 X2 Q →
+  SetUnfoldElemOf x (cprod X1 X2) (P ∧ Q).
+Proof.
+  intros ??; constructor.
+  by rewrite elem_of_boolset_cprod, (set_unfold_elem_of x.1 X1 P),
+    (set_unfold_elem_of x.2 X2 Q).
+Qed.
+
 Global Typeclasses Opaque boolset_elem_of.
 Global Opaque boolset_empty boolset_singleton boolset_union
-  boolset_intersection boolset_difference.
+  boolset_intersection boolset_difference boolset_cprod.
diff --git a/stdpp/gmap.v b/stdpp/gmap.v
index dd093390f3057e82d7d0ea740ce0616a77cbd333..ed811569ed3149e4e8852a2451335566bec925cc 100644
--- a/stdpp/gmap.v
+++ b/stdpp/gmap.v
@@ -823,4 +823,25 @@ Section gset.
   Qed.
 End gset.
 
+Section gset_cprod.
+  Context `{Countable A, Countable B}.
+
+  Global Instance gset_cprod : CProd (gset A) (gset B) (gset (A * B)) :=
+    λ X Y, set_bind (λ e1, set_map (e1,.) Y) X.
+
+  Lemma elem_of_gset_cprod (X : gset A) (Y : gset B) x :
+    x ∈ cprod X Y ↔ x.1 ∈ X ∧ x.2 ∈ Y.
+  Proof. unfold cprod, gset_cprod. destruct x. set_solver. Qed.
+
+  Global Instance set_unfold_gset_cprod (X : gset A) (Y : gset B) x (P : Prop) Q :
+    SetUnfoldElemOf x.1 X P → SetUnfoldElemOf x.2 Y Q →
+    SetUnfoldElemOf x (cprod X Y) (P ∧ Q).
+  Proof using.
+    intros ??; constructor.
+    by rewrite elem_of_gset_cprod, (set_unfold_elem_of x.1 X P),
+      (set_unfold_elem_of x.2 Y Q).
+  Qed.
+
+End gset_cprod.
+
 Global Typeclasses Opaque gset.
diff --git a/stdpp/list.v b/stdpp/list.v
index 9b25e6d9dc04d99d29a8c2dfb80b33fcca4e85bc..1b4c3ecd08422b93acf707f108ffda7763a0a440 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -224,6 +224,17 @@ Global Instance list_join: MJoin list :=
   fix go A (ls : list (list A)) : list A :=
   match ls with [] => [] | l :: ls => l ++ @mjoin _ go _ ls end.
 
+(** The Cartesian product on lists satisfies (lemma [elem_of_list_cprod]):
+
+  x ∈ cprod l k ↔ x.1 ∈ l ∧ x.2 ∈ k
+
+There are little meaningful things to say about the order of the elements in
+[cprod] (so there are no lemmas for that). It thus only makes sense to use
+[cprod] when treating the lists as a set-like structure (i.e., up to duplicates
+and permutations). *)
+Global Instance list_cprod {A B} : CProd (list A) (list B) (list (A * B)) :=
+  λ l k, x ← l; (x,.) <$> k.
+
 Definition mapM `{MBind M, MRet M} {A B} (f : A → M B) : list A → M (list B) :=
   fix go l :=
   match l with [] => mret [] | x :: l => y ← f x; k ← go l; mret (y :: k) end.
@@ -1035,6 +1046,19 @@ Proof.
   - rewrite <-!reverse_snoc, <-!reverse_app, <-!(assoc_L (++)). by f_equal.
 Qed.
 
+(** The Cartesian product *)
+(** Correspondence to [list_prod] from the stdlib, a version that does not use
+the [CProd] class for the interface, nor the monad classes for the definition *)
+Lemma list_cprod_list_prod {B} l (k : list B) : cprod l k = list_prod l k.
+Proof. unfold cprod, list_cprod. induction l; f_equal/=; auto. Qed.
+
+Lemma elem_of_list_cprod {B} l (k : list B) (x : A * B) :
+  x ∈ cprod l k ↔ x.1 ∈ l ∧ x.2 ∈ k.
+Proof.
+  rewrite list_cprod_list_prod, !elem_of_list_In.
+  destruct x. apply in_prod_iff.
+Qed.
+
 (** ** Properties of the [NoDup] predicate *)
 Lemma NoDup_nil : NoDup (@nil A) ↔ True.
 Proof. split; constructor. Qed.
diff --git a/stdpp/sets.v b/stdpp/sets.v
index a681d7c5d44cee30e62de36281636503d1b7060a..6ee9590c0cf52d1ae144456a3b87b304cc3df368 100644
--- a/stdpp/sets.v
+++ b/stdpp/sets.v
@@ -287,6 +287,15 @@ Section set_unfold_list.
     intros ??; constructor.
     by rewrite elem_of_app, (set_unfold_elem_of x l P), (set_unfold_elem_of x k Q).
   Qed.
+  Global Instance set_unfold_list_cprod {B} (x : A * B) l (k : list B) P Q :
+    SetUnfoldElemOf x.1 l P → SetUnfoldElemOf x.2 k Q →
+    SetUnfoldElemOf x (cprod l k) (P ∧ Q).
+  Proof.
+    intros ??; constructor.
+    by rewrite elem_of_list_cprod, (set_unfold_elem_of x.1 l P),
+      (set_unfold_elem_of x.2 k Q).
+  Qed.
+
   Global Instance set_unfold_included l k (P Q : A → Prop) :
     (∀ x, SetUnfoldElemOf x l (P x)) → (∀ x, SetUnfoldElemOf x k (Q x)) →
     SetUnfold (l ⊆ k) (∀ x, P x → Q x).
@@ -1105,6 +1114,24 @@ Section set_monad.
     rewrite elem_of_mapM. intros Hl1. revert l2.
     induction Hl1; inv 1; constructor; auto.
   Qed.
+
+  Global Instance monadset_cprod {A B} : CProd (M A) (M B) (M (A * B)) := λ X Y,
+    x ← X; fmap (x,.) Y.
+
+  Lemma elem_of_monadset_cprod {A B} (X : M A) (Y : M B) (x : A * B) :
+    x ∈ cprod X Y ↔ x.1 ∈ X ∧ x.2 ∈ Y.
+  Proof. unfold cprod, monadset_cprod. destruct x; set_solver. Qed.
+
+  Global Instance set_unfold_monadset_cprod {A B} (X : M A) (Y : M B) P Q x :
+    SetUnfoldElemOf x.1 X P →
+    SetUnfoldElemOf x.2 Y Q →
+    SetUnfoldElemOf x (cprod X Y) (P ∧ Q).
+  Proof.
+    constructor.
+    by rewrite elem_of_monadset_cprod, (set_unfold_elem_of x.1 X P),
+      (set_unfold_elem_of x.2 Y Q).
+  Qed.
+
 End set_monad.
 
 (** Finite sets *)