natrS -> natr1

math-comp · Sep 5, 2022 · 7127fc7 · 7127fc7
1 parent ce7f6b2
commit 7127fc7
Show file tree

Hide file tree

Showing 9 changed files with 21 additions and 25 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -54,7 +54,7 @@
 - in `topology.v`:
   + lemmas `open_setIS`, `open_setSI`, `closed_setIS`, `closed_setSI`
 - in `mathcomp_extra.v`:
-  + lemmas `natrS`, `natSr`
+  + lemmas `natr1`, `nat1r`
 
 ### Changed
 

diff --git a/theories/ereal.v b/theories/ereal.v
@@ -1126,20 +1126,16 @@ case: x => /= [x [_/posnumP[d] dP] |[d [dreal dP]] |[d [dreal dP]]]; last 2 firs
       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_floor _) _; rewrite Nfloor.
-    by rewrite  -natrS ler_nat.
+    by apply; rewrite (lt_le_trans (lt_succ_floor _))// Nfloor natr1 ler_nat.
   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_floor _) _; rewrite Nfloor.
-  by rewrite -natrS ler_nat.
+  by apply; rewrite (lt_le_trans (lt_succ_floor _))// Nfloor natr1 ler_nat.
 have /ZnatP [N Nfloor] : floor (d%:num^-1) \is a Znat.
   by rewrite Znat_def floor_ge0.
-exists N => // n leNn; have gt0Sn : (0 < n%:R + 1 :> R)%R.
-  by apply: ltr_spaddr => //; exact/ler0n.
-apply: dP; last first.
-  by rewrite eq_sym addrC -subr_eq subrr eq_sym; apply/invr_neq0/lt0r_neq0.
+exists N => // n leNn; apply: dP; last first.
+  by rewrite eq_sym addrC -subr_eq subrr eq_sym; exact/invr_neq0/lt0r_neq0.
 rewrite /= opprD addrA subrr distrC subr0 gtr0_norm; last by rewrite invr_gt0.
 rewrite -[ltLHS]mulr1 ltr_pdivr_mull // -ltr_pdivr_mulr // div1r.
 by rewrite (lt_le_trans (lt_succ_floor _))// Nfloor ler_add// ler_nat.

diff --git a/theories/exp.v b/theories/exp.v
@@ -134,7 +134,7 @@ case: n => [|n].
 rewrite subrXX addrK -mulrBr; congr (_ * _).
 rewrite -(big_mkord xpredT (fun i => (h + z) ^+ (n - i) * z ^+ i)).
 rewrite big_nat_recr //= subnn expr0 -addrA -mulrBl.
-rewrite natSr opprD addrA subrr sub0r mulNr.
+rewrite -nat1r opprD addrA subrr sub0r mulNr.
 rewrite mulr_natl -[in X in _ *+ X](subn0 n) -sumr_const_nat -sumrB.
 rewrite pseries_diffs_P1 mulr_sumr !big_mkord; apply: eq_bigr => i _.
 rewrite mulrCA; congr (_ * _).
@@ -394,7 +394,7 @@ Qed.
 Lemma expRMm n x : expR (n%:R * x) = expR x ^+ n.
 Proof.
 elim: n x => [x|n IH x] /=; first by rewrite mul0r expr0 expR0.
-by rewrite exprS natSr mulrDl mul1r expRD IH.
+by rewrite exprS -nat1r mulrDl mul1r expRD IH.
 Qed.
 
 Lemma expR_gt1 x:  (1 < expR x) = (0 < x).
@@ -606,7 +606,7 @@ Qed.
 Lemma exp_fun_mulrn a n : 0 < a -> exp_fun a n%:R = a ^+ n.
 Proof.
 move=> a0; elim: n => [|n ih]; first by rewrite mulr0n expr0 exp_funr0.
-by rewrite natrS exprSr exp_funD// ih exp_funr1.
+by rewrite -natr1 exprSr exp_funD// ih exp_funr1.
 Qed.
 
 End ExpFun.

diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
@@ -1228,7 +1228,7 @@ rewrite predeqE => r; split => [/= /[!in_itv]/= /andP[nr rn1]|].
     rewrite ler_pdivr_mulr// (le_trans _ (floor_le _))//.
     by rewrite -(@gez0_abs (floor _))// floor_ge0 mulr_ge0// (le_trans _ nr).
   rewrite ltr_pdivl_mulr// (lt_le_trans (lt_succ_floor _))//.
-  rewrite [in leRHS]natrS ler_add2r// -(@gez0_abs (floor _))// floor_ge0.
+  rewrite -[in leRHS]natr1 ler_add2r// -(@gez0_abs (floor _))// floor_ge0.
   by rewrite mulr_ge0// (le_trans _ nr).
 - rewrite -bigcup_set => -[/= k] /[!mem_index_iota] /andP[nk kn].
   rewrite in_itv /= => /andP[knr rkn]; rewrite in_itv /=; apply/andP; split.
@@ -1381,7 +1381,7 @@ have xAnK : x \in A n (Ordinal K).
     rewrite ler_pdivr_mulr// (le_trans _ (floor_le _))//.
     by rewrite -(@gez0_abs (floor _))// floor_ge0 mulr_ge0// ltW.
   rewrite ltr_pdivl_mulr// (lt_le_trans (lt_succ_floor _))//.
-  rewrite [in leRHS]natrS ler_add2r// -{1}(@gez0_abs (floor _))//.
+  rewrite -[in leRHS]natr1 ler_add2r// -{1}(@gez0_abs (floor _))//.
   by rewrite floor_ge0// mulr_ge0// ltW.
 have /[!mem_index_enum]/(_ isT) := An0 (Ordinal K).
 apply/negP.
@@ -1497,7 +1497,7 @@ have : fine (f x) < n%:R.
   near: n.
   exists `|floor (fine (f x))|.+1%N => //= p /=.
   rewrite -(@ler_nat R); apply: lt_le_trans.
-  rewrite natrS (_ : `| _ |%:R  = (floor (fine (f x)))%:~R); last first.
+  rewrite -natr1 (_ : `| _ |%:R  = (floor (fine (f x)))%:~R); last first.
     by rewrite -[in RHS](@gez0_abs (floor _))// floor_ge0//; exact/fine_ge0/f0.
   by rewrite lt_succ_floor.
 rewrite -lte_fin (fineK fxfin) => fxn.
@@ -1509,7 +1509,7 @@ rewrite (@le_lt_trans _ _ (1 / 2 ^+ n)) //.
     rewrite ler_subr_addl -mulrBl -lee_fin (fineK fxfin) -rfx lee_fin.
     rewrite (le_trans _ k1)// ler_pmul2r// -(@natrB _ _ 1) // ler_nat subn1.
     by rewrite leq_pred.
-  by rewrite ler_subl_addr -mulrDl -lee_fin -natSr fineK// ltW// -rfx lte_fin.
+  by rewrite ler_subl_addr -mulrDl -lee_fin nat1r fineK// ltW// -rfx lte_fin.
 by near: n; exact: near_infty_natSinv_expn_lt.
 Unshelve. all: by end_near. Qed.
 
@@ -3113,7 +3113,7 @@ apply/negP; rewrite -ltNge.
 rewrite -[X in _ * X](@fineK _ (mu (E `&` D))); last first.
   by rewrite fin_numElt muEDoo andbT (lt_le_trans _ (measure_ge0 _ _)).
 rewrite lte_fin -ltr_pdivr_mulr.
-  rewrite natrS natr_absz ger0_norm.
+  rewrite -natr1 natr_absz ger0_norm.
     by rewrite (le_lt_trans (ceil_ge _))// ltr_addl.
   by rewrite ceil_ge0// divr_ge0//; apply/le0R/measure_ge0; exact: measurableI.
 rewrite -lte_fin fineK.
@@ -3441,7 +3441,7 @@ move=> mf; split=> [iDf0|Df0].
         - rewrite inE unitfE fine_eq0 // abse_eq0 ft0/=; apply/fine_gt0.
           by rewrite lt_neqAle abse_ge0 -ge0_fin_numE// eq_sym abse_eq0 ft0.
         - by rewrite inE unitfE invr_eq0 pnatr_eq0 /= invr_gt0.
-      rewrite invrK /m natrS natr_absz ger0_norm ?ceil_ge0//.
+      rewrite invrK /m -natr1 natr_absz ger0_norm ?ceil_ge0//.
       apply: (@le_trans _ _ ((fine `|f t|)^-1 + 1)%R); first by rewrite ler_addl.
       by rewrite ler_add2r// ceil_ge.
     by split => //; apply: contraTN nft => /eqP ->; rewrite abse0 -ltNge.

diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
@@ -562,7 +562,7 @@ move=> x rx; apply/esym/eqP; rewrite eq_le (itvP (rx 0%N _))// andbT.
 apply/ler_addgt0Pl => e e_gt0; rewrite -ler_subl_addl ltW//.
 have := rx `|floor e^-1%R|%N I; rewrite /= in_itv => /andP[/le_lt_trans->]//.
 rewrite ler_add2l ler_opp2 -lef_pinv ?invrK//; last by rewrite qualifE.
-by rewrite natrS natr_absz ger0_norm ?floor_ge0 ?invr_ge0 1?ltW// lt_succ_floor.
+by rewrite -natr1 natr_absz ger0_norm ?floor_ge0 ?invr_ge0 1?ltW// lt_succ_floor.
 Qed.
 
 Lemma itv_bnd_open_bigcup (R : realType) b (r s : R) :
@@ -575,7 +575,7 @@ apply/seteqP; split => [x/=|]; last first.
 rewrite in_itv/= => /andP[sx xs]; exists `|ceil ((s - x)^-1)|%N => //=.
 rewrite in_itv/= sx/= ler_subr_addl addrC -ler_subr_addl.
 rewrite -[in X in _ <= X](invrK (s - x)) ler_pinv.
-- rewrite natrS natr_absz ger0_norm; last first.
+- rewrite -natr1 natr_absz ger0_norm; last first.
     by rewrite ceil_ge0// invr_ge0 subr_ge0 ltW.
   by rewrite (@le_trans _ _ (ceil (s - x)^-1)%:~R)// ?ler_addl// ceil_ge.
 - by rewrite inE unitfE ltr0n andbT pnatr_eq0.

diff --git a/theories/mathcomp_extra.v b/theories/mathcomp_extra.v
@@ -148,10 +148,10 @@ Proof. by move->. Qed.
 Lemma eqbRL (b1 b2 : bool) : b1 = b2 -> b2 -> b1.
 Proof. by move->. Qed.
 
-Lemma natrS (R : ringType) (n : nat) : (n.+1%:R = n%:R + 1 :> R)%R.
+Lemma natr1 (R : ringType) (n : nat) : (n%:R + 1 = n.+1%:R :> R)%R.
 Proof. by rewrite GRing.mulrSr. Qed.
 
-Lemma natSr (R : ringType) (n : nat) : (n.+1%:R = 1 + n%:R :> R)%R.
+Lemma nat1r (R : ringType) (n : nat) : (1 + n%:R = n.+1%:R :> R)%R.
 Proof. by rewrite GRing.mulrS. Qed.
 
 (***************************)

diff --git a/theories/reals.v b/theories/reals.v
@@ -726,7 +726,7 @@ Proof.
 move=> yx; exists `|floor (x - y)^-1|%N.
 rewrite -ltr_subr_addl -{2}(invrK (x - y)%R) ltf_pinv ?qualifE ?ltr0n//.
   by rewrite invr_gt0 subr_gt0.
-rewrite natrS natr_absz ger0_norm.
+rewrite -natr1 natr_absz ger0_norm.
   by rewrite floor_ge0 invr_ge0 subr_ge0 ltW.
 by rewrite -RfloorE lt_succ_Rfloor.
 Qed.

diff --git a/theories/sequences.v b/theories/sequences.v
@@ -1204,7 +1204,7 @@ have /uoo[N _ NuA] : \oo [set m | `|ceil A|.+1 <= m]%N by exists `|ceil A|.+1.
 near=> n; have /NuA : (N <= n)%N by near: n; exact: nbhs_infty_ge.
 rewrite /= -(ler_nat R); apply: le_trans.
 have [A0|A0] := leP 0%R A; last by rewrite (le_trans (ltW A0)).
-by rewrite natrS natr_absz ger0_norm// ?ceil_ge0// ler_paddr// ceil_ge.
+by rewrite -natr1 natr_absz ger0_norm// ?ceil_ge0// ler_paddr// ceil_ge.
 Unshelve. all: by end_near. Qed.
 
 Lemma nat_cvgPpinfty (u : nat^nat) :

diff --git a/theories/set_interval.v b/theories/set_interval.v
@@ -413,7 +413,7 @@ Proof.
 rewrite predeqE => y; split=> /=; last first.
   by move=> [n _]/=; rewrite in_itv => /andP[xy yn]; rewrite in_itv /= xy.
 rewrite in_itv /= andbT => xy; exists (`|floor y|%N.+1) => //=.
-rewrite in_itv /= xy /= natrS.
+rewrite in_itv /= xy /= -natr1.
 have [y0|y0] := ltP 0 y; last by rewrite (le_lt_trans y0)// ltr_spaddr.
 by rewrite natr_absz ger0_norm ?lt_succ_floor// floor_ge0 ltW.
 Qed.