Fixing confusion about idempotency of abs.

Co-Authored-By: yannl35133 <[email protected]>
eladrion · Oct 22, 2023 · 2a3d4cf · 2a3d4cf
1 parent f202dcb
commit 2a3d4cf
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/theories/Numbers/Integer/Abstract/ZSgnAbs.v b/theories/Numbers/Integer/Abstract/ZSgnAbs.v
@@ -143,11 +143,14 @@ Proof.
  intros n. destruct_max n; rewrite ? opp_involutive; auto with relations.
 Qed.
 
-Lemma abs_involutive : forall n, abs (abs n) == abs n.
+Lemma abs_idemp : forall n, abs (abs n) == abs n.
 Proof.
  intros. apply abs_eq. apply abs_nonneg.
 Qed.
 
+#[deprecated(since="8.19", note="Use abs_idemp")]
+Notation abs_involutive := abs_idemp.
+
 Lemma abs_spec : forall n,
   (0 <= n /\ abs n == n) \/ (n < 0 /\ abs n == -n).
 Proof.