Merge PR coq#18192: Fixing confusion about idempotency of abs

Reviewed-by: proux01 Ack-by: yannl35133 Co-authored-by: proux01 <[email protected]>
SkySkimmer · Oct 24, 2023 · b7c0814 · b7c0814
2 parents 684781f + 2a3d4cf
commit b7c0814
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.