gen floor_le0

math-comp · Jul 12, 2024 · f9c14c1 · f9c14c1
1 parent 9df3f3f
commit f9c14c1
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 10 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -50,9 +50,11 @@
   + lemma `lt_succ_floor`: conclusion changed to match `lt_succ_floor` in MathComp,
     generalized to `archiDomainType`
   + generalized to `archiDomainType`:
-    lemmas `floor_ge0`, `floor_le0`, `floor_lt0`, `floor_natz`,
+    lemmas `floor_ge0`, `floor_lt0`, `floor_natz`,
     `floor_ge_int`, `floor_neq0`, `floor_lt_int`, `ceil_ge`, `ceil_ge0`, `ceil_gt0`,
     `ceil_le0`, `ceil_ge_int`, `ceil_lt_int`, `ceilN`, `abs_ceil_ge`
+  + generalized to `archiDomainType` and precondition generalized:
+    + `floor_le0`
 
 ### Renamed
 

diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
@@ -399,8 +399,10 @@ Proof. by rewrite ltNge floor_ge_int -ltNge. Qed.
 Lemma floor_ge0 x : (0 <= Num.floor x) = (0 <= x).
 Proof. by rewrite -floor_ge_int. Qed.
 
-Lemma floor_le0 x : x <= 0 -> Num.floor x <= 0.
-Proof. by move/Num.Theory.floor_le; rewrite Num.Theory.floor0. Qed.
+Lemma floor_le0 x : x < 1 -> Num.floor x <= 0.
+Proof.
+by rewrite (_ : 1 = 1%:~R)// floor_lt_int -ltzD1 add0r => /le_lt_trans; exact.
+Qed.
 
 Lemma floor_lt0 x : x < 0 -> Num.floor x < 0.
 Proof. by rewrite -floor_lt_int. Qed.

diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
@@ -1580,15 +1580,13 @@ case/cvg_ex => /= l; have [l0|l0] := leP 0%R l.
   rewrite normrN lerBrDl addSnnS [leRHS]ger0_norm ?ler0n//.
   rewrite natrD lerD// ?ler1n// ger0_norm // (le_trans (ceil_ge _)) //.
   by rewrite -(@gez0_abs (ceil _)) // ceil_ge0.
-- move/cvgrPdist_lt => /(_ _ ltr01) -[n _].
-  move=> /(_ (`|floor l|.+1 + n)%N) /= /(_ (leq_addl _ _)).
-  rewrite approx_x.
-  apply/negP; rewrite -leNgt distrC (le_trans _ (lerB_normD _ _)) //.
+- move=> /cvgrPdist_lt/(_ _ ltr01)[n _].
+  move=> /(_ (`|floor l|.+1 + n)%N)/(_ (leq_addl _ _)); apply/negP.
+  rewrite approx_x -leNgt distrC (le_trans _ (lerB_normD _ _))//.
   rewrite normrN lerBrDl addSnnS [leRHS]ger0_norm ?ler0n//.
-  rewrite natrD lerD// ?ler1n// ler0_norm //; last by rewrite ltW.
-  rewrite (@le_trans _ _ (- floor l)%:~R) //.
+  rewrite natrD lerD ?ler1n// ltr0_norm// (@le_trans _ _ (- floor l)%:~R)//.
     by rewrite mulrNz lerNl opprK ge_floor.
-  by rewrite -(@lez0_abs (floor _))// floor_le0 // ltW.
+  by rewrite -(@lez0_abs (floor _))// floor_le0// (lt_le_trans l0).
 Qed.
 
 Lemma ecvg_approx (f0 : forall x, D x -> (0 <= f x)%E) x :