deprecate floor_ge0

math-comp · Jun 26, 2024 · cfc65e4 · cfc65e4
1 parent 1c429eb
commit cfc65e4
Showing 1 changed file with 6 additions and 4 deletions.
diff --git a/theories/reals.v b/theories/reals.v
@@ -557,7 +557,7 @@ Proof. by rewrite floor0. Qed.
 Lemma floor1 : floor (1 : R) = 1.
 Proof. by rewrite floor1. Qed.
 
-Lemma floor_ge0 x : (0 <= floor x) = (0 <= x).
+Lemma __deprecated__floor_ge0 x : (0 <= floor x) = (0 <= x).
 Proof. by rewrite -floor_ge_int// num_real. Qed.
 
 Lemma floor_le0 x : x <= 0 -> floor x <= 0.
@@ -574,9 +574,9 @@ Proof. by move=> a b ab; rewrite Num.Theory.floor_le. Qed.
 Lemma floor_neq0 x : (floor x != 0) = (x < 0) || (x >= 1).
 Proof.
 apply/idP/orP => [|[x0|/le_floor r1]]; first rewrite neq_lt => /orP[x0|x0].
-- by left; apply: contra_lt x0; rewrite floor_ge0.
+- by left; apply: contra_lt x0; rewrite -floor_ge_int ?num_real.
 - by right; rewrite (le_trans _ (ge_floor _)) ?num_real// ler1z -gtz0_ge1.
-- by rewrite lt_eqF//; apply: contra_lt x0; rewrite floor_ge0.
+- by rewrite lt_eqF//; apply: contra_lt x0; rewrite -floor_ge_int ?num_real.
 - by rewrite gt_eqF// (lt_le_trans _ r1)// floor1.
 Qed.
 
@@ -595,11 +595,13 @@ move=> yx; exists `|floor (x - y)^-1|%N.
 rewrite -ltrBrDl -{2}(invrK (x - y)%R) ltf_pV2 ?qualifE/= ?ltr0n//.
   by rewrite invr_gt0 subr_gt0.
 rewrite -natr1 natr_absz ger0_norm.
-  by rewrite floor_ge0 invr_ge0 subr_ge0 ltW.
+  by rewrite -floor_ge_int ?num_real// invr_ge0 subr_ge0 ltW.
 by rewrite intr1 lt_succ_floor ?num_real.
 Qed.
 
 End FloorTheory.
+#[deprecated(since="mathcomp-analysis 1.3.0", note="use `floor_ge_int` instead")]
+Notation floor_ge0 := __deprecated__floor_ge0 (only parsing).
 
 Section CeilTheory.
 Variable R : realType.