diff --git a/CHANGELOG.md b/CHANGELOG.md
index 8c4667d41f5b987bce9c418eb5907ac217a864d0..0ee29fd569e59035ded05e46582fb281497bf2e6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -60,6 +60,8 @@ Noteworthy additions and changes:
 - Rename `fin_maps.singleton_proper` into `singletonM_proper` since it concerns
   `singletonM` and to avoid overlap with `sets.singleton_proper`.
 - Add `wn R` for weakly normalizing elements w.r.t. a relation `R`.
+- Add `encode_Z`/`decode_Z` functions to encode elements of a countable type
+  as integers `Z`, in analogy with `encode_nat`/`decode_nat`.
 
 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/theories/countable.v b/theories/countable.v
index 9b5373c4257d65e912594272f728f0169fbb4ba1..3c87aab98b46421eebd5b2070d8db04253f404f7 100644
--- a/theories/countable.v
+++ b/theories/countable.v
@@ -12,15 +12,16 @@ Hint Mode Countable ! - : typeclass_instances.
 Arguments encode : simpl never.
 Arguments decode : simpl never.
 
-Definition encode_nat `{Countable A} (x : A) : nat :=
-  pred (Pos.to_nat (encode x)).
-Definition decode_nat `{Countable A} (i : nat) : option A :=
-  decode (Pos.of_nat (S i)).
 Instance encode_inj `{Countable A} : Inj (=) (=) (encode (A:=A)).
 Proof.
   intros x y Hxy; apply (inj Some).
   by rewrite <-(decode_encode x), Hxy, decode_encode.
 Qed.
+
+Definition encode_nat `{Countable A} (x : A) : nat :=
+  pred (Pos.to_nat (encode x)).
+Definition decode_nat `{Countable A} (i : nat) : option A :=
+  decode (Pos.of_nat (S i)).
 Instance encode_nat_inj `{Countable A} : Inj (=) (=) (encode_nat (A:=A)).
 Proof. unfold encode_nat; intros x y Hxy; apply (inj encode); lia. Qed.
 Lemma decode_encode_nat `{Countable A} (x : A) : decode_nat (encode_nat x) = Some x.
@@ -30,6 +31,15 @@ Proof.
   by rewrite Pos2Nat.id, decode_encode.
 Qed.
 
+Definition encode_Z `{Countable A} (x : A) : Z :=
+  Zpos (encode x).
+Definition decode_Z `{Countable A} (i : Z) : option A :=
+  match i with Zpos i => decode i | _ => None end.
+Instance encode_Z_inj `{Countable A} : Inj (=) (=) (encode_Z (A:=A)).
+Proof. unfold encode_Z; intros x y Hxy; apply (inj encode); lia. Qed.
+Lemma decode_encode_Z `{Countable A} (x : A) : decode_Z (encode_Z x) = Some x.
+Proof. apply decode_encode. Qed.
+
 (** * Choice principles *)
 Section choice.
   Context `{Countable A} (P : A → Prop).