diff --git a/theories/numbers.v b/theories/numbers.v
index f8f237cf24e5873899fce1cc7f6633e42d037984..4acc4adf9dc0a68ba9a8e1de202a109041294494 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -553,8 +553,7 @@ 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.
+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.