Consistently block `simpl` on all `Z` operations

We used to do this some operations (Z.add, Z.mul), but not for others (Z.sub, Z.of_nat); this MR blocks simpl consistently for all operations involving Z that I could think of.

The rationale for blocking everything is that simpl produces very bad results, e.g. try:

Require Import ZArith.

Eval simpl in (fun n y => Z.of_nat (S n) + y)%Z.
(*
Yields:

  fun (n : nat) (y : Z) =>
       match y with
       | 0%Z => Z.pos (Pos.of_succ_nat n)
       | Z.pos y' => Z.pos (Pos.of_succ_nat n + y')
       | Z.neg y' => Z.pos_sub (Pos.of_succ_nat n) y'
       end
*)

Note that blocking simpl for Z.of_nat used to break lia and omega in the past, see https://github.com/coq/coq/issues/5039. For lia this has been fixed, but for omega not yet. However, in !37 (merged) we decided to use lia everywhere in both std++ and Iris because it's faster, and moreover, I believe the Coq devs intend to deprecate omega in favor of lia in the future. So, I don't think we should care about omega anymore.

I also updated the item "Side-effects" in the README to document that we block simpl on Z operations.

@jjourdan @jung Any objections to this MR?

I have fixes for Iris, iris-examples, Iron, lambdaRust (which are mostly a couple of one-liners). I thus would like to merge this ASAP (so I don't get merge conflicts on my fixes).

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.