From 7127fc77a0bdebf86119b7c34bf5d0f6e4445182 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 6 Sep 2022 00:36:47 +0900 Subject: [PATCH] natrS -> natr1 --- CHANGELOG_UNRELEASED.md | 2 +- theories/ereal.v | 12 ++++-------- theories/exp.v | 6 +++--- theories/lebesgue_integral.v | 12 ++++++------ theories/lebesgue_measure.v | 4 ++-- theories/mathcomp_extra.v | 4 ++-- theories/reals.v | 2 +- theories/sequences.v | 2 +- theories/set_interval.v | 2 +- 9 files changed, 21 insertions(+), 25 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index e82105c4f..1e13dea62 100644 --- 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 index 72617f678..8aec80000 100644 --- 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 index 01e0268a8..e99f0a64e 100644 --- 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 index 0d2bb9908..b40449688 100644 --- 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 index 597d19451..6c5421d8a 100644 --- 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 index 567d181c1..47bf46425 100644 --- 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 index ca0b9c57b..0ff1b78ea 100644 --- 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 index 00e2197b7..5f76422e1 100644 --- 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 index 16d5d7a16..558a3b143 100644 --- 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.