diff --git a/CHANGELOG.md b/CHANGELOG.md
index 68862da27c64735a6934894b78a16c185e0a4ccc..b728eee9548e24044261ceb012d1d6428279fbd9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3,7 +3,8 @@ API-breaking change is listed.
 
 ## std++ master
 
-- Add lemmas for lookup on `mjoin` for lists (by Michael Sammler).
+- Add `bool_to_Z` that converts true to 1 and false to 0. (by Michael Sammler)
+- Add lemmas for lookup on `mjoin` for lists. (by Michael Sammler)
 - Rename `Is_true_false` → `Is_true_false_2` and `eq_None_ne_Some` → `eq_None_ne_Some_1`.
 
 The following `sed` script should perform most of the renaming
diff --git a/theories/numbers.v b/theories/numbers.v
index d3e773410c76e5b6a6dd8b8989cab9223b7085ae..f8f237cf24e5873899fce1cc7f6633e42d037984 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -543,6 +543,21 @@ Proof. intros ?. rewrite <-Z.lxor_lor by done. by rewrite Z.add_nocarry_lxor. Qe
 Lemma Z_opp_lnot a : -a - 1 = Z.lnot a.
 Proof. pose proof (Z.add_lnot_diag a). lia. Qed.
 
+(** ** [bool_to_Z] *)
+Definition bool_to_Z (b : bool) : Z :=
+  if b then 1 else 0.
+
+Lemma bool_to_Z_bound b : 0 ≤ bool_to_Z b < 2.
+Proof. destruct b; simpl; lia. Qed.
+Lemma bool_to_Z_eq_0 b : bool_to_Z b = 0 ↔ b = false.
+Proof. destruct b; naive_solver. Qed.
+Lemma bool_to_Z_neq_0 b : bool_to_Z b ≠ 0 ↔ b = true.
+Proof. destruct b; naive_solver. Qed.
+Lemma bool_to_Z_spec b n:
+  Z.testbit (bool_to_Z b) n = bool_decide (n = 0) && b.
+Proof. by destruct b, n. Qed.
+
+
 Local Close Scope Z_scope.
 
 (** * Injectivity of casts *)