diff --git a/README.md b/README.md
index b84ff7f472bbc9708664e1d8c9659f645641b186..2dbdd6719eba7b6cb1a313f9a451f38c1d9982dd 100644
--- a/README.md
+++ b/README.md
@@ -33,6 +33,13 @@ Notably:
 * The behavior of `Program` is tweaked: `Unset Transparent Obligations`,
   `Obligation Tactic := idtac`, `Add Search Blacklist "_obligation_"`.  See
   [`base.v`](theories/base.v) for further details.
+* It blocks `simpl` on all operations on integers `Z` (by setting
+  `Arguments op : simpl never`). We do this because `simpl` tends to expose
+  their internals (e.g. try `simpl` on `Z.of_nat (S n) + y`).
+  As a consequence of blocking `simpl`, due to
+  [Coq bug #5039](https://github.com/coq/coq/issues/5039) the `omega` tactic
+  sometimes fails. We do not consider this an issue since we use `lia` (for
+  which the aforementioned Coq bug was fixed) instead of `omega` anywhere.
 
 ## Prerequisites
 
diff --git a/theories/numbers.v b/theories/numbers.v
index 0fd07d35c25dc4770dc3a88ba506342ca25347e1..b577e015a38b61c34f177acceb56213343af70a3 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -283,17 +283,31 @@ Proof.
   split. apply Z.quot_pos; lia. trans x; auto. apply Z.quot_lt; lia.
 Qed.
 
-(* Note that we cannot disable simpl for [Z.of_nat] as that would break
-tactics as [lia]. *)
+Arguments Z.pred : simpl never.
+Arguments Z.succ : simpl never.
+Arguments Z.of_nat : simpl never.
 Arguments Z.to_nat : simpl never.
 Arguments Z.mul : simpl never.
 Arguments Z.add : simpl never.
+Arguments Z.sub : simpl never.
 Arguments Z.opp : simpl never.
 Arguments Z.pow : simpl never.
 Arguments Z.div : simpl never.
 Arguments Z.modulo : simpl never.
 Arguments Z.quot : simpl never.
 Arguments Z.rem : simpl never.
+Arguments Z.shiftl : simpl never.
+Arguments Z.shiftr : simpl never.
+Arguments Z.gcd : simpl never.
+Arguments Z.lcm : simpl never.
+Arguments Z.min : simpl never.
+Arguments Z.max : simpl never.
+Arguments Z.lor : simpl never.
+Arguments Z.land : simpl never.
+Arguments Z.lxor : simpl never.
+Arguments Z.lnot : simpl never.
+Arguments Z.square : simpl never.
+Arguments Z.abs : simpl never.
 
 Lemma Z_to_nat_neq_0_pos x : Z.to_nat x ≠ 0%nat → 0 < x.
 Proof. by destruct x. Qed.