change inequality in ereal_{d,}nbhs

- from strict to large - also in {p,n}infty_{d,}nbhs closed #122
math-comp · May 13, 2022 · 55724fb · 55724fb
1 parent 77b5614
commit 55724fb
Show file tree

Hide file tree

Showing 7 changed files with 213 additions and 161 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -88,6 +88,14 @@
   + generalize `eq_nneseries`, `nneseries0`
 - in `mathcomp_extra.v`:
   + generalize `card_fset_sum1`
+- in `ereal.v`:
+  + lemmas `lee_paddl`, `lte_addl`, `lee_paddr`, `lte_paddr`, `lee_lt_add`
+- in `ereal.v`:
+  + definitions `ereal_dnbhs` and `ereal_nbhs` changed to use large inequality instead
+    of strict inequality
+- in `normedtype.v`:
+  + definitions `pinfty_dnbhs` and `ninfty_nbhs` changed to use large inequality instead
+    of strict inequality
 
 ### Renamed
 

diff --git a/theories/derive.v b/theories/derive.v
@@ -171,7 +171,7 @@ move=> /diff_locallyP [dfc]; rewrite -addrA.
 rewrite (littleo_bigO_eqo (cst (1 : R))); last first.
   apply/eqOP; near=> k; rewrite /cst [`|1|]normr1 mulr1.
   near=> y; rewrite ltW //; near: y; apply/nbhs_normP.
-  exists k; first by near: k; exists 0.
+  exists k => /=; first by near: k; exact: nbhs_pinfty_gt.
   by move=> ? /=; rewrite -ball_normE /= sub0r normrN.
 rewrite addfo; first by move=> /eqolim; rewrite cvg_comp_shift add0r.
 by apply/eqolim0P; apply: (cvg_trans (dfc 0)); rewrite linear0.
@@ -1307,8 +1307,8 @@ have imf_sup : has_sup imf.
   split; first by exists (f a); apply/imageP; rewrite /= in_itv /= lexx.
   have [M [Mreal imfltM]] : bounded_set (f @` `[a, b]).
     by apply/compact_bounded/continuous_compact => //; exact: segment_compact.
-  exists (M + 1) => y /imfltM yleM.
-  by rewrite (le_trans _ (yleM _ _)) ?ler_norm ?ltr_addl.
+  exists (M + 1); apply/ubP => y /imfltM/= yleM.
+  by rewrite (le_trans _ (yleM _ _)) ?ler_addl ?ler_norm.
 have [|imf_ltsup] := pselect (exists2 c, c \in `[a, b]%R & f c = sup imf).
   move=> [c cab fceqsup]; exists c => // t tab; rewrite fceqsup.
   by apply/sup_upper_bound => //; exact/imageP.

diff --git a/theories/ereal.v b/theories/ereal.v
@@ -1588,6 +1588,10 @@ move: x y a b => [x| |] [y| |] [a| |] [b| |] _ _ //=; rewrite ?(ltey, ltNye)//.
 by rewrite !lte_fin; exact: ltr_le_add.
 Qed.
 
+Lemma lee_lt_add a b x y : a \is a fin_num -> b \is a fin_num ->
+  a <= x -> b < y -> a + b < x + y.
+Proof. by move=> afin bin xa yb; rewrite (addeC a) (addeC x) lte_le_add. Qed.
+
 Lemma lee_sub x y z u : x <= y -> u <= z -> x - z <= y - u.
 Proof.
 move: x y z u => -[x| |] -[y| |] -[z| |] -[u| |] //=; rewrite ?(leey,leNye)//.
@@ -2645,6 +2649,18 @@ exists (PosNum xy); apply/negP; rewrite -ltNge lte_fin -ltr_subr_addl.
 by rewrite ltr_pdivr_mulr // ltr_pmulr ?subr_gt0 // ltr1n.
 Qed.
 
+Lemma lee_paddl y x z : 0 <= x -> y <= z -> y <= x + z.
+Proof. by move=> *; rewrite -[y]add0e lee_add. Qed.
+
+Lemma lte_paddl y x z : 0 <= x -> y < z -> y < x + z.
+Proof. by move=> x0 /lt_le_trans; apply; rewrite lee_paddl. Qed.
+
+Lemma lee_paddr y x z : 0 <= x -> y <= z -> y <= z + x.
+Proof. by move=> *; rewrite addeC lee_paddl. Qed.
+
+Lemma lte_paddr y x z : 0 <= x -> y < z -> y < z + x.
+Proof. by move=> *; rewrite addeC lte_paddl. Qed.
+
 Lemma lte_spaddr z x y : z \is a fin_num -> 0 < y -> z <= x -> z < x + y.
 Proof.
 move: z y x => [z| |] [y| |] [x| |] _ //=; rewrite ?(lte_fin, lte_fin, ltey) //.
@@ -3371,14 +3387,14 @@ Local Open Scope classical_set_scope.
 Definition ereal_dnbhs (x : \bar R) (P : \bar R -> Prop) : Prop :=
   match x with
     | r%:E => r^' (fun r => P r%:E)
-    | +oo => exists M, M \is Num.real /\ forall y, M%:E < y -> P y
-    | -oo => exists M, M \is Num.real /\ forall y, y < M%:E -> P y
+    | +oo => exists M, M \is Num.real /\ forall y, M%:E <= y -> P y
+    | -oo => exists M, M \is Num.real /\ forall y, y <= M%:E -> P y
   end.
 Definition ereal_nbhs (x : \bar R) (P : \bar R -> Prop) : Prop :=
   match x with
     | x%:E => nbhs x (fun r => P r%:E)
-    | +oo => exists M, M \is Num.real /\ forall y, M%:E < y -> P y
-    | -oo => exists M, M \is Num.real /\ forall y, y < M%:E -> P y
+    | +oo => exists M, M \is Num.real /\ forall y, M%:E <= y -> P y
+    | -oo => exists M, M \is Num.real /\ forall y, y <= M%:E -> P y
   end.
 Canonical ereal_ereal_filter :=
   FilteredType (extended R) (extended R) (ereal_nbhs).
@@ -3407,63 +3423,63 @@ case=> [x||].
   by move=> P Q PQ /xS; apply => y /PQ.
 - apply Build_ProperFilter.
     move=> P [x [xr xP]] //; exists (x + 1)%:E; apply xP => /=.
-    by rewrite lte_fin ltr_addl.
-  split=> /= [|P Q [MP [MPr gtMP]] [MQ [MQr gtMQ]] |P Q sPQ [M [Mr gtM]]].
-  + by exists 0%R.
+    by rewrite lee_fin ler_addl.
+  split=> /= [|P Q [MP [MPr geMP]] [MQ [MQr geMQ]] |P Q sPQ [M [Mr geM]]].
+  + by exists 0%R; rewrite real0.
   + have [MP0|MP0] := eqVneq MP 0%R.
       have [MQ0|MQ0] := eqVneq MQ 0%R.
-        by exists 0%R; split => // x x0; split;
-          [apply/gtMP; rewrite MP0 | apply/gtMQ; rewrite MQ0].
+        by exists 0%R; rewrite real0; split => // x x0; split;
+        [apply/geMP; rewrite MP0 | apply/geMQ; rewrite MQ0].
       exists `|MQ|%R; rewrite realE normr_ge0; split => // x MQx; split.
-        by apply: gtMP; rewrite (le_lt_trans _ MQx) // MP0 lee_fin.
-      by apply gtMQ; rewrite (le_lt_trans _ MQx)// lee_fin real_ler_normr ?lexx.
+        by apply: geMP; rewrite (le_trans _ MQx) // MP0 lee_fin.
+      by apply geMQ; rewrite (le_trans _ MQx)// lee_fin real_ler_normr ?lexx.
     have [MQ0|MQ0] := eqVneq MQ 0%R.
       exists `|MP|%R; rewrite realE normr_ge0; split => // x MPx; split.
-      by apply gtMP; rewrite (le_lt_trans _ MPx)// lee_fin real_ler_normr ?lexx.
-      by apply gtMQ; rewrite (le_lt_trans _ MPx) // lee_fin MQ0.
+      by apply geMP; rewrite (le_trans _ MPx)// lee_fin real_ler_normr ?lexx.
+      by apply geMQ; rewrite (le_trans _ MPx) // lee_fin MQ0.
     have {}MP0 : (0 < `|MP|)%R by rewrite normr_gt0.
     have {}MQ0 : (0 < `|MQ|)%R by rewrite normr_gt0.
     exists (Num.max (PosNum MP0) (PosNum MQ0))%:num.
     rewrite realE /= ge0 /=; split => //.
     case=> [r| |//].
-    * rewrite lte_fin/= num_max num_lt_maxl /= => /andP[MPx MQx]; split.
-      by apply/gtMP; rewrite lte_fin (le_lt_trans _ MPx)// real_ler_normr ?lexx.
-      by apply/gtMQ; rewrite lte_fin (le_lt_trans _ MQx)// real_ler_normr ?lexx.
-    * by move=> _; split; [apply/gtMP | apply/gtMQ].
-  + by exists M; split => // ? /gtM /sPQ.
+    * rewrite lee_fin /= num_max num_le_maxl /= => /andP[MPx MQx]; split.
+      by apply/geMP; rewrite lee_fin (le_trans _ MPx)// real_ler_normr ?lexx.
+      by apply/geMQ; rewrite lee_fin (le_trans _ MQx)// real_ler_normr ?lexx.
+    * by move=> _; split; [apply/geMP | apply/geMQ].
+  + by exists M; split => // ? /geM /sPQ.
 - apply Build_ProperFilter.
   + move=> P [M [Mr ltMP]]; exists (M - 1)%:E.
-    by apply: ltMP; rewrite lte_fin gtr_addl oppr_lt0.
-  + split=> /= [|P Q [MP [MPr ltMP]] [MQ [MQr ltMQ]] |P Q sPQ [M [Mr ltM]]].
-    * by exists 0%R.
+    by apply: ltMP; rewrite lee_fin ger_addl oppr_le0.
+  + split=> /= [|P Q [MP [MPr leMP]] [MQ [MQr leMQ]] |P Q sPQ [M [Mr leM]]].
+    * by exists 0%R; rewrite real0.
     * have [MP0|MP0] := eqVneq MP 0%R.
         have [MQ0|MQ0] := eqVneq MQ 0%R.
-          by exists 0%R; split => // x x0; split;
-          [apply/ltMP; rewrite MP0 | apply/ltMQ; rewrite MQ0].
+          by exists 0%R; rewrite real0; split => // x x0; split;
+          [apply/leMP; rewrite MP0 | apply/leMQ; rewrite MQ0].
         exists (- `|MQ|)%R; rewrite realN realE normr_ge0; split => // x xMQ.
         split.
-          by apply ltMP; rewrite (lt_le_trans xMQ)// lee_fin MP0 ler_oppl oppr0.
-       apply ltMQ; rewrite (lt_le_trans xMQ) // lee_fin ler_oppl -normrN.
+          by apply leMP; rewrite (le_trans xMQ)// lee_fin MP0 ler_oppl oppr0.
+       apply leMQ; rewrite (le_trans xMQ) // lee_fin ler_oppl -normrN.
        by rewrite real_ler_normr ?realN // lexx.
     * have [MQ0|MQ0] := eqVneq MQ 0%R.
         exists (- `|MP|)%R; rewrite realN realE normr_ge0; split => // x MPx.
         split.
-          apply ltMP; rewrite (lt_le_trans MPx) // lee_fin ler_oppl -normrN.
+          apply leMP; rewrite (le_trans MPx) // lee_fin ler_oppl -normrN.
           by rewrite real_ler_normr ?realN // lexx.
-        by apply ltMQ; rewrite (lt_le_trans MPx) // lee_fin MQ0 ler_oppl oppr0.
+        by apply leMQ; rewrite (le_trans MPx) // lee_fin MQ0 ler_oppl oppr0.
       have {}MP0 : (0 < `|MP|)%R by rewrite normr_gt0.
       have {}MQ0 : (0 < `|MQ|)%R by rewrite normr_gt0.
       exists (- (Num.max (PosNum MP0) (PosNum MQ0))%:num)%R.
       rewrite realN realE /= ge0 /=; split => //.
       case=> [r|//|].
-      - rewrite lte_fin ltr_oppr num_max num_lt_maxl => /andP[].
-        rewrite ltr_oppr => MPx; rewrite ltr_oppr => MQx; split.
-          apply/ltMP; rewrite lte_fin (lt_le_trans MPx) //= ler_oppl -normrN.
+      - rewrite lee_fin ler_oppr num_max num_le_maxl => /andP[].
+        rewrite ler_oppr => MPx; rewrite ler_oppr => MQx; split.
+          apply/leMP; rewrite lee_fin (le_trans MPx) //= ler_oppl -normrN.
           by rewrite real_ler_normr ?realN // lexx.
-        apply/ltMQ; rewrite lte_fin (lt_le_trans MQx) //= ler_oppl -normrN.
+        apply/leMQ; rewrite lee_fin (le_trans MQx) //= ler_oppl -normrN.
         by rewrite real_ler_normr ?realN // lexx.
-      - by move=> _; split; [apply/ltMP | apply/ltMQ].
-    * by exists M; split => // x /ltM /sPQ.
+      - by move=> _; split; [apply/leMP | apply/leMQ].
+    * by exists M; split => // x /leM /sPQ.
 Qed.
 Typeclasses Opaque ereal_dnbhs.
 
@@ -3498,32 +3514,34 @@ move: p => -[p| [M [Mreal MA]] | [M [Mreal MA]]] //=.
   apply/nbhs_ballP; exists (e%:num / 2) => //= r per.
   apply/nbhs_ballP; exists (e%:num / 2) => //= x rex.
   apply/ballA/(@ball_splitl _ _ r) => //; exact/ball_sym.
-- exists (M + 1)%R; split; first by rewrite realD.
-  move=> -[x| _ |_] //=; last by exists M.
-  rewrite lte_fin => M'x /=.
-  apply/nbhs_ballP; exists 1%R => //= y x1y.
-  apply MA; rewrite lte_fin.
-  rewrite addrC -ltr_subr_addl in M'x.
-  rewrite (lt_le_trans M'x) // ler_subl_addl addrC -ler_subl_addl.
-  rewrite (le_trans _ (ltW x1y)) // real_ler_norm // realB //.
-    rewrite ltr_subr_addr in M'x.
-    rewrite -comparabler0 (@comparabler_trans _ (M + 1)%R) //.
-      by rewrite /Order.comparable (ltW M'x) orbT.
-    by rewrite comparabler0 realD.
-  by rewrite num_real. (* where we really use realFieldType *)
-- exists (M - 1)%R; split; first by rewrite realB.
-  move=> -[x| _ |_] //=; last by exists M.
-  rewrite lte_fin => M'x /=.
-  apply/nbhs_ballP; exists 1%R => //= y x1y.
-  apply MA; rewrite lte_fin.
-  rewrite ltr_subr_addl in M'x.
-  rewrite (le_lt_trans _ M'x) // addrC -ler_subl_addl.
-  rewrite (le_trans _ (ltW x1y)) // distrC real_ler_norm // realB //.
+- exists (M + 1)%R; split; first by rewrite realD // real1.
+  move=> -[x| _ |] //=.
+    rewrite lee_fin => M'x /=.
+    apply/nbhs_ballP; exists 1%R => //= y x1y.
+    apply MA; rewrite lee_fin.
+    rewrite addrC -ler_subr_addl in M'x.
+    rewrite (le_trans M'x) // ler_subl_addl addrC -ler_subl_addl.
+    rewrite (le_trans _ (ltW x1y)) // real_ler_norm // realB //.
+      rewrite ler_subr_addr in M'x.
+      rewrite -comparabler0 (@comparabler_trans _ (M + 1)%R) //.
+        by rewrite /Order.comparable M'x orbT.
+      by rewrite comparabler0 realD // real1.
     by rewrite num_real. (* where we really use realFieldType *)
-  rewrite addrC -ltr_subr_addr in M'x.
-  rewrite -comparabler0 (@comparabler_trans _ (M - 1)%R) //.
-    by rewrite /Order.comparable (ltW M'x).
-  by rewrite comparabler0 realB.
+  by exists M.
+- exists (M - 1)%R; split; first by rewrite realB // real1.
+  move=> -[x| _ |] //=.
+    rewrite lee_fin => M'x /=.
+    apply/nbhs_ballP; exists 1%R => //= y x1y.
+    apply MA; rewrite lee_fin.
+    rewrite ler_subr_addl in M'x.
+    rewrite (le_trans _ M'x) // addrC -ler_subl_addl.
+    rewrite (le_trans _ (ltW x1y)) // distrC real_ler_norm // realB //.
+      by rewrite num_real. (* where we really use realFieldType *)
+    rewrite addrC -ler_subr_addr in M'x.
+    rewrite -comparabler0 (@comparabler_trans _ (M - 1)%R) //.
+      by rewrite /Order.comparable M'x.
+    by rewrite comparabler0 realB // real1.
+  by exists M.
 Qed.
 
 Definition ereal_topologicalMixin : Topological.mixin_of (@ereal_nbhs R) :=
@@ -3551,19 +3569,19 @@ case: x => [r /=| |].
 - rewrite predeqE => S; split=> [[M [Mreal MS]]|[x [M [Mreal Mx]] <-]].
     exists (-%E @` S).
       exists (- M)%R; rewrite realN Mreal; split => // x Mx.
-      by exists (- x); [apply MS; rewrite lte_oppl | rewrite oppeK].
+      by exists (- x); [apply MS; rewrite lee_oppl | rewrite oppeK].
     rewrite predeqE => x; split=> [[y [z Sz <- <-]]|Sx]; first by rewrite oppeK.
     by exists (- x); [exists x | rewrite oppeK].
   exists (- M)%R; rewrite realN; split => // y yM.
-  exists (- y); by [apply Mx; rewrite lte_oppr|rewrite oppeK].
+  exists (- y); by [apply Mx; rewrite lee_oppr|rewrite oppeK].
 - rewrite predeqE => S; split=> [[M [Mreal MS]]|[x [M [Mreal Mx]] <-]].
     exists (-%E @` S).
       exists (- M)%R; rewrite realN Mreal; split => // x Mx.
-      by exists (- x); [apply MS; rewrite lte_oppr | rewrite oppeK].
+      by exists (- x); [apply MS; rewrite lee_oppr | rewrite oppeK].
     rewrite predeqE => x; split=> [[y [z Sz <- <-]]|Sx]; first by rewrite oppeK.
     by exists (- x); [exists x | rewrite oppeK].
   exists (- M)%R; rewrite realN; split => // y yM.
-  exists (- y); by [apply Mx; rewrite lte_oppl|rewrite oppeK].
+  exists (- y); by [apply Mx; rewrite lee_oppl|rewrite oppeK].
 Qed.
 
 Lemma nbhsNKe (R : realFieldType) (z : \bar R) (A : set (\bar R)) :
@@ -3926,12 +3944,15 @@ Lemma nbhs_oo_up_e1 (A : set (\bar R)) (e : {posnum R}) : (e%:num <= 1)%R ->
   ereal_ball +oo e%:num `<=` A -> nbhs +oo A.
 Proof.
 move=> e1 ooeA.
-exists (fine (expand (1 - e%:num)%R)); rewrite num_real; split => //.
-case => [r | | //].
-- rewrite fine_expand; last first.
-    by rewrite ger0_norm ?ltr_subl_addl ?ltr_addr // subr_ge0.
-  by move=> ?; exact/ooeA/expand_ereal_ball_pinfty.
-- by move=> _; exact/ooeA/ereal_ball_center.
+exists (fine (expand (1 - e%:num / 2)%R)); rewrite num_real; split => //.
+have e21 : (`|1 - e%:num / 2| < 1)%R.
+  rewrite ger0_norm; first by rewrite ltr_subl_addl ltr_addr.
+  by rewrite subr_ge0 ler_pdivr_mulr// mul1r (le_trans e1)// ler1n.
+case => [r| _ |//]; last exact/ooeA/ereal_ball_center.
+rewrite fine_expand // => er; apply/ooeA/expand_ereal_ball_pinfty => //.
+rewrite (lt_le_trans _ er)// lt_expand ?inE; last exact/ltW.
+  by rewrite ler_lt_sub// ltr_pdivr_mulr// ltr_pmulr// ltr1n.
+by rewrite ger0_norm ?subr_ge0// ler_subl_addl addrC -ler_subl_addl subrr.
 Qed.
 
 Lemma nbhs_oo_down_e1 (A : set (\bar R)) (e : {posnum R}) : (e%:num <= 1)%R ->
@@ -4194,12 +4215,12 @@ rewrite predeq2E => x A; split.
       by rewrite subr_gt0 (le_lt_trans _ (contract_lt1 M)) // ler_norm.
     case=> [r| |]/=.
     * rewrite /ereal_ball [_ +oo]/= => rM1.
-      apply: MA; rewrite lte_fin.
+      apply: MA; rewrite lee_fin.
       rewrite ger0_norm in rM1; last first.
         by rewrite subr_ge0 // (le_trans _ (contract_le1 r%:E)) // ler_norm.
       rewrite ltr_subl_addr addrC addrCA addrC -ltr_subl_addr subrr in rM1.
       rewrite subr_gt0 in rM1.
-      by rewrite -lte_fin -lt_contract.
+      by rewrite -lee_fin -le_contract ltW.
     * by rewrite /ereal_ball /= subrr normr0 => h; exact: MA.
     * rewrite /ereal_ball /= opprK => h {MA}.
       exfalso.
@@ -4214,12 +4235,12 @@ rewrite predeq2E => x A; split.
     case=> [r| |].
     * rewrite /ereal_ball => /= rM1.
       apply MA.
-      rewrite lte_fin.
+      rewrite lee_fin.
       rewrite ler0_norm in rM1; last first.
         rewrite ler_subl_addl addr0 ltW //.
         by move: (contract_lt1 r); rewrite ltr_norml => /andP[].
       rewrite opprB opprK -ltr_subl_addl addrK in rM1.
-      by rewrite -lte_fin -lt_contract.
+      by rewrite -lee_fin -le_contract ltW.
     * rewrite /ereal_ball /= -opprD normrN => h {MA}.
       exfalso.
       move: h; apply/negP.
@@ -4316,14 +4337,14 @@ case: x => /= [x [_/posnumP[d] dP] |[d [dreal dP]] |[d [dreal dP]]]; last 2 firs
     have /ZnatP [N Nfloor] : floor (Num.max d 0%R) \is a Znat.
       by rewrite Znat_def floor_ge0 le_maxr lexx orbC.
     exists N.+1 => // n ltNn; apply: dP.
-    have /le_lt_trans : (d <= Num.max d 0)%R by rewrite le_maxr lexx.
-    apply; apply: lt_le_trans (lt_succ_Rfloor _) _; rewrite RfloorE Nfloor.
+    have /le_trans : (d <= Num.max d 0)%R by rewrite le_maxr lexx.
+    apply; apply: le_trans (ltW (lt_succ_Rfloor _)) _; rewrite RfloorE Nfloor.
     by rewrite -(@natrD R N 1) ler_nat addn1.
   have /ZnatP [N Nfloor] : floor (Num.max (- d)%R 0%R) \is a Znat.
     by rewrite Znat_def floor_ge0 le_maxr lexx orbC.
-  exists N.+1 => // n ltNn; apply: dP; rewrite lte_fin ltr_oppl.
-  have /le_lt_trans : (- d <= Num.max (- d) 0)%R by rewrite le_maxr lexx.
-  apply; apply: lt_le_trans (lt_succ_Rfloor _) _; rewrite RfloorE Nfloor.
+  exists N.+1 => // n ltNn; apply: dP; rewrite lee_fin ler_oppl.
+  have /le_trans : (- d <= Num.max (- d) 0)%R by rewrite le_maxr lexx.
+  apply; apply: le_trans (ltW (lt_succ_Rfloor _)) _; rewrite RfloorE Nfloor.
   by rewrite -(@natrD R N 1) ler_nat addn1.
 have /ZnatP [N Nfloor] : floor (d%:num^-1) \is a Znat.
   by rewrite Znat_def floor_ge0.

diff --git a/theories/exp.v b/theories/exp.v
@@ -57,7 +57,7 @@ apply: series_le_cvg Kzxn _ _ => [//=| /= n|].
     rewrite !normrM normr_id mulrAC mulfK // normr_eq0 expf_eq0 andbC.
     by case: ltrgt0P zLx; rewrite //= normr_lt0.
   do! (apply: ler_pmul || apply: mulr_ge0 || rewrite invr_ge0) => //.
-  by apply Kf => //; rewrite (lt_le_trans _ (ler_norm _))// ltr_addl.
+  by apply Kf => //; rewrite (le_trans _ (ler_norm _))// ler_addl.
 have F : `|z / x| < 1.
   by rewrite normrM normfV ltr_pdivr_mulr ?mul1r // (le_lt_trans _ zLx).
 rewrite (_ : (fun _ => _) = geometric `|K + 1| `|z / x|); last first.