From 83e8892161c8ef3903e302c82a2a7a43f2708d67 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 21 May 2020 23:32:46 +0900 Subject: three lemmas that we found useful in the context of the mathcomp-analysis project --- mathcomp/algebra/ssralg.v | 3 +++ mathcomp/algebra/ssrnum.v | 6 ++++++ 2 files changed, 9 insertions(+) (limited to 'mathcomp') diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index 2bde8dd..0e71c86 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -764,6 +764,9 @@ Proof. by rewrite opprD addrA addrK. Qed. Lemma subrKA z x y : (x - z) + (z + y) = x + y. Proof. by rewrite addrA addrNK. Qed. +Lemma subr_trans z x y : (x - z) + (z - y) = x - y. +Proof. by rewrite addrA addrNK. Qed. + Lemma addr0_eq x y : x + y = 0 -> - x = y. Proof. by rewrite -[-x]addr0 => <-; rewrite addKr. Qed. diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index e1e5992..41199eb 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -3754,6 +3754,12 @@ Proof. by rewrite lter_norml !lter_sub_addl. Qed. Definition lter_distl := (ler_distl, ltr_distl). +Lemma ltr_distW x y e : `|x - y| < e -> y - e < x. +Proof. by rewrite ltr_distl => /andP[]. Qed. + +Lemma ler_distW x y e : `|x - y| <= e -> y - e <= x. +Proof. by rewrite ler_distl => /andP[]. Qed. + Lemma exprn_even_ge0 n x : ~~ odd n -> 0 <= x ^+ n. Proof. by move=> even_n; rewrite real_exprn_even_ge0 ?num_real. Qed. -- cgit v1.2.3 From a65958322cb6ee84f3ebbb68d1fb4867749cf1a0 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 22 May 2020 03:52:40 +0900 Subject: tentative change of naming convention and add variants --- mathcomp/algebra/ssralg.v | 3 --- mathcomp/algebra/ssrnum.v | 22 ++++++++++++++++++++-- 2 files changed, 20 insertions(+), 5 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index 0e71c86..2bde8dd 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -764,9 +764,6 @@ Proof. by rewrite opprD addrA addrK. Qed. Lemma subrKA z x y : (x - z) + (z + y) = x + y. Proof. by rewrite addrA addrNK. Qed. -Lemma subr_trans z x y : (x - z) + (z - y) = x - y. -Proof. by rewrite addrA addrNK. Qed. - Lemma addr0_eq x y : x + y = 0 -> - x = y. Proof. by rewrite -[-x]addr0 => <-; rewrite addKr. Qed. diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 41199eb..7a41745 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -3754,12 +3754,30 @@ Proof. by rewrite lter_norml !lter_sub_addl. Qed. Definition lter_distl := (ler_distl, ltr_distl). -Lemma ltr_distW x y e : `|x - y| < e -> y - e < x. +Lemma ltr_dist_addl x y e : `|x - y| < e -> x < y + e. Proof. by rewrite ltr_distl => /andP[]. Qed. -Lemma ler_distW x y e : `|x - y| <= e -> y - e <= x. +Lemma ler_dist_addl x y e : `|x - y| <= e -> x <= y + e. Proof. by rewrite ler_distl => /andP[]. Qed. +Lemma ltr_distr_addl x y e : `|x - y| < e -> y < x + e. +Proof. by rewrite distrC => /ltr_dist_addl. Qed. + +Lemma ler_distr_addl x y e : `|x - y| <= e -> y <= x + e. +Proof. by rewrite distrC => /ler_dist_addl. Qed. + +Lemma ltr_dist_subl x y e : `|x - y| < e -> x - e < y. +Proof. by move/ltr_dist_addl; rewrite -ltr_subl_addr. Qed. + +Lemma ler_dist_subl x y e : `|x - y| <= e -> x - e <= y. +Proof. by move/ler_dist_addl; rewrite -ler_subl_addr. Qed. + +Lemma ltr_distr_subr x y e : `|x - y| < e -> y - e < x. +Proof. by rewrite distrC => /ltr_dist_subl. Qed. + +Lemma ler_distr_subr x y e : `|x - y| <= e -> y - e <= x. +Proof. by rewrite distrC => /ler_dist_subl. Qed. + Lemma exprn_even_ge0 n x : ~~ odd n -> 0 <= x ^+ n. Proof. by move=> even_n; rewrite real_exprn_even_ge0 ?num_real. Qed. -- cgit v1.2.3 From 3d77e498c075af6f642b3239acf4b18503c1e6bc Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 2 Jun 2020 18:14:22 +0900 Subject: another lemma about norm from mathcomp-analysis --- mathcomp/algebra/ssrnum.v | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'mathcomp') diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 7a41745..5047868 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -3778,6 +3778,12 @@ Proof. by rewrite distrC => /ltr_dist_subl. Qed. Lemma ler_distr_subr x y e : `|x - y| <= e -> y - e <= x. Proof. by rewrite distrC => /ler_dist_subl. Qed. +Lemma norm_lt_eqF (x y : R) : `|x| < y -> (x == - y = false) * (x == y = false). +Proof. +move=> x1; split; last by rewrite lt_eqF // (le_lt_trans (ler_norm _) x1). +by move: x1; rewrite ltr_norml => /andP[? ?]; rewrite gt_eqF. +Qed. + Lemma exprn_even_ge0 n x : ~~ odd n -> 0 <= x ^+ n. Proof. by move=> even_n; rewrite real_exprn_even_ge0 ?num_real. Qed. -- cgit v1.2.3 From e5165bd0bb3ba31c7ecc95f99e1c43353feca987 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 3 Jun 2020 04:48:09 +0900 Subject: add real_* variants --- mathcomp/algebra/ssrnum.v | 64 +++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 54 insertions(+), 10 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 5047868..361394a 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -2894,7 +2894,19 @@ rewrite real_ltNge ?real_ler_norml // negb_and -?real_ltNge ?realN //. by rewrite orbC ltr_oppr. Qed. -Definition real_lter_normr := (real_ler_normr, real_ltr_normr). +Definition real_lter_normr := (real_ler_normr, real_ltr_normr). + +Lemma real_gtr_norm x y : x \is real -> `|x| < y -> x < y. +Proof. by move=> ?; case/real_ltr_normlP. Qed. + +Lemma real_gtrNnorm x y : x \is real -> `|x| < y -> - y < x. +Proof. by move=> ?; case/real_ltr_normlP => //; rewrite ltr_oppl. Qed. + +Lemma real_ger_norm x y : x \is real -> `|x| <= y -> x <= y. +Proof. by move=> ?; case/real_ler_normlP. Qed. + +Lemma real_gerNnorm x y : x \is real -> `|x| <= y -> - y <= x. +Proof. by move=> ?; case/real_ler_normlP => //; rewrite ler_oppl. Qed. Lemma real_ler_distl x y e : x - y \is real -> (`|x - y| <= e) = (y - e <= x <= y + e). @@ -2906,6 +2918,30 @@ Proof. by move=> Rxy; rewrite real_lter_norml // !lter_sub_addl. Qed. Definition real_lter_distl := (real_ler_distl, real_ltr_distl). +Lemma real_ltr_dist_addl x y e : x - y \is real -> `|x - y| < e -> x < y + e. +Proof. by move=> ?; rewrite real_ltr_distl // => /andP[]. Qed. + +Lemma real_ler_dist_addl x y e : x - y \is real -> `|x - y| <= e -> x <= y + e. +Proof. by move=> ?; rewrite real_ler_distl // => /andP[]. Qed. + +Lemma real_ltr_distr_addl x y e : x - y \is real -> `|x - y| < e -> y < x + e. +Proof. by rewrite realBC (distrC x) => ? /real_ltr_dist_addl; apply. Qed. + +Lemma real_ler_distr_addl x y e : x - y \is real -> `|x - y| <= e -> y <= x + e. +Proof. by rewrite realBC distrC => ? /real_ler_dist_addl; apply. Qed. + +Lemma real_ltr_dist_subl x y e : x - y \is real -> `|x - y| < e -> x - e < y. +Proof. by move/real_ltr_dist_addl; rewrite ltr_sub_addr; apply. Qed. + +Lemma real_ler_dist_subl x y e : x - y \is real -> `|x - y| <= e -> x - e <= y. +Proof. by move/real_ler_dist_addl; rewrite ler_sub_addr; apply. Qed. + +Lemma real_ltr_distr_subr x y e : x - y \is real -> `|x - y| < e -> y - e < x. +Proof. by rewrite realBC distrC => ? /real_ltr_dist_subl; apply. Qed. + +Lemma real_ler_distr_subr x y e : x - y \is real -> `|x - y| <= e -> y - e <= x. +Proof. by rewrite realBC distrC => ? /real_ler_dist_subl; apply. Qed. + (* GG: pointless duplication }-( *) Lemma eqr_norm_id x : (`|x| == x) = (0 <= x). Proof. by rewrite ger0_def. Qed. Lemma eqr_normN x : (`|x| == - x) = (x <= 0). Proof. by rewrite ler0_def. Qed. @@ -3738,6 +3774,14 @@ Lemma ltr_normlP x y : reflect ((-x < y) * (x < y)) (`|x| < y). Proof. exact: real_ltr_normlP. Qed. Arguments ltr_normlP {x y}. +Lemma gtr_norm x y : `|x| < y -> x < y. Proof. exact: real_gtr_norm. Qed. + +Lemma gtrNnorm x y : `|x| < y -> - y < x. Proof. exact: real_gtrNnorm. Qed. + +Lemma ger_norm x y : `|x| <= y -> x <= y. Proof. exact: real_ger_norm. Qed. + +Lemma gerNnorm x y : `|x| <= y -> - y <= x. Proof. exact: real_gerNnorm. Qed. + Lemma ler_normr x y : (x <= `|y|) = (x <= y) || (x <= - y). Proof. by rewrite leNgt ltr_norml negb_and -!leNgt orbC ler_oppr. Qed. @@ -3755,30 +3799,30 @@ Proof. by rewrite lter_norml !lter_sub_addl. Qed. Definition lter_distl := (ler_distl, ltr_distl). Lemma ltr_dist_addl x y e : `|x - y| < e -> x < y + e. -Proof. by rewrite ltr_distl => /andP[]. Qed. +Proof. exact: real_ltr_dist_addl. Qed. Lemma ler_dist_addl x y e : `|x - y| <= e -> x <= y + e. -Proof. by rewrite ler_distl => /andP[]. Qed. +Proof. exact: real_ler_dist_addl. Qed. Lemma ltr_distr_addl x y e : `|x - y| < e -> y < x + e. -Proof. by rewrite distrC => /ltr_dist_addl. Qed. +Proof. exact: real_ltr_distr_addl. Qed. Lemma ler_distr_addl x y e : `|x - y| <= e -> y <= x + e. -Proof. by rewrite distrC => /ler_dist_addl. Qed. +Proof. exact: real_ler_distr_addl. Qed. Lemma ltr_dist_subl x y e : `|x - y| < e -> x - e < y. -Proof. by move/ltr_dist_addl; rewrite -ltr_subl_addr. Qed. +Proof. exact: real_ltr_dist_subl. Qed. Lemma ler_dist_subl x y e : `|x - y| <= e -> x - e <= y. -Proof. by move/ler_dist_addl; rewrite -ler_subl_addr. Qed. +Proof. exact: real_ler_dist_subl. Qed. Lemma ltr_distr_subr x y e : `|x - y| < e -> y - e < x. -Proof. by rewrite distrC => /ltr_dist_subl. Qed. +Proof. exact: real_ltr_distr_subr. Qed. Lemma ler_distr_subr x y e : `|x - y| <= e -> y - e <= x. -Proof. by rewrite distrC => /ler_dist_subl. Qed. +Proof. exact: real_ler_distr_subr. Qed. -Lemma norm_lt_eqF (x y : R) : `|x| < y -> (x == - y = false) * (x == y = false). +Lemma gt_norm_eqF (x y : R) : `|x| < y -> (x == - y = false) * (x == y = false). Proof. move=> x1; split; last by rewrite lt_eqF // (le_lt_trans (ler_norm _) x1). by move: x1; rewrite ltr_norml => /andP[? ?]; rewrite gt_eqF. -- cgit v1.2.3 From 0a999b90fb9517849b70a8bb28895b0e905af2b4 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 4 Jun 2020 19:25:53 +0900 Subject: fix naming --- mathcomp/algebra/ssrnum.v | 90 ++++++++++++++++++++++------------------------- 1 file changed, 42 insertions(+), 48 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 361394a..8184577 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -2896,16 +2896,16 @@ Qed. Definition real_lter_normr := (real_ler_normr, real_ltr_normr). -Lemma real_gtr_norm x y : x \is real -> `|x| < y -> x < y. +Lemma real_ltr_normlW x y : x \is real -> `|x| < y -> x < y. Proof. by move=> ?; case/real_ltr_normlP. Qed. -Lemma real_gtrNnorm x y : x \is real -> `|x| < y -> - y < x. +Lemma real_ltrNnormlW x y : x \is real -> `|x| < y -> - y < x. Proof. by move=> ?; case/real_ltr_normlP => //; rewrite ltr_oppl. Qed. -Lemma real_ger_norm x y : x \is real -> `|x| <= y -> x <= y. +Lemma real_ler_normlW x y : x \is real -> `|x| <= y -> x <= y. Proof. by move=> ?; case/real_ler_normlP. Qed. -Lemma real_gerNnorm x y : x \is real -> `|x| <= y -> - y <= x. +Lemma real_lerNnormlW x y : x \is real -> `|x| <= y -> - y <= x. Proof. by move=> ?; case/real_ler_normlP => //; rewrite ler_oppl. Qed. Lemma real_ler_distl x y e : @@ -2918,29 +2918,29 @@ Proof. by move=> Rxy; rewrite real_lter_norml // !lter_sub_addl. Qed. Definition real_lter_distl := (real_ler_distl, real_ltr_distl). -Lemma real_ltr_dist_addl x y e : x - y \is real -> `|x - y| < e -> x < y + e. +Lemma real_ltr_distl_addr x y e : x - y \is real -> `|x - y| < e -> x < y + e. Proof. by move=> ?; rewrite real_ltr_distl // => /andP[]. Qed. -Lemma real_ler_dist_addl x y e : x - y \is real -> `|x - y| <= e -> x <= y + e. +Lemma real_ler_distl_addr x y e : x - y \is real -> `|x - y| <= e -> x <= y + e. Proof. by move=> ?; rewrite real_ler_distl // => /andP[]. Qed. -Lemma real_ltr_distr_addl x y e : x - y \is real -> `|x - y| < e -> y < x + e. -Proof. by rewrite realBC (distrC x) => ? /real_ltr_dist_addl; apply. Qed. +Lemma real_ltr_distl_addrC x y e : x - y \is real -> `|x - y| < e -> y < x + e. +Proof. by rewrite realBC (distrC x) => ? /real_ltr_distl_addr; apply. Qed. -Lemma real_ler_distr_addl x y e : x - y \is real -> `|x - y| <= e -> y <= x + e. -Proof. by rewrite realBC distrC => ? /real_ler_dist_addl; apply. Qed. +Lemma real_ler_distl_addrC x y e : x - y \is real -> `|x - y| <= e -> y <= x + e. +Proof. by rewrite realBC distrC => ? /real_ler_distl_addr; apply. Qed. -Lemma real_ltr_dist_subl x y e : x - y \is real -> `|x - y| < e -> x - e < y. -Proof. by move/real_ltr_dist_addl; rewrite ltr_sub_addr; apply. Qed. +Lemma real_ltr_distl_subl x y e : x - y \is real -> `|x - y| < e -> x - e < y. +Proof. by move/real_ltr_distl_addr; rewrite ltr_sub_addr; apply. Qed. -Lemma real_ler_dist_subl x y e : x - y \is real -> `|x - y| <= e -> x - e <= y. -Proof. by move/real_ler_dist_addl; rewrite ler_sub_addr; apply. Qed. +Lemma real_ler_distl_subl x y e : x - y \is real -> `|x - y| <= e -> x - e <= y. +Proof. by move/real_ler_distl_addr; rewrite ler_sub_addr; apply. Qed. -Lemma real_ltr_distr_subr x y e : x - y \is real -> `|x - y| < e -> y - e < x. -Proof. by rewrite realBC distrC => ? /real_ltr_dist_subl; apply. Qed. +Lemma real_ltr_distl_sublC x y e : x - y \is real -> `|x - y| < e -> y - e < x. +Proof. by rewrite realBC distrC => ? /real_ltr_distl_subl; apply. Qed. -Lemma real_ler_distr_subr x y e : x - y \is real -> `|x - y| <= e -> y - e <= x. -Proof. by rewrite realBC distrC => ? /real_ler_dist_subl; apply. Qed. +Lemma real_ler_distl_sublC x y e : x - y \is real -> `|x - y| <= e -> y - e <= x. +Proof. by rewrite realBC distrC => ? /real_ler_distl_subl; apply. Qed. (* GG: pointless duplication }-( *) Lemma eqr_norm_id x : (`|x| == x) = (0 <= x). Proof. by rewrite ger0_def. Qed. @@ -3774,59 +3774,53 @@ Lemma ltr_normlP x y : reflect ((-x < y) * (x < y)) (`|x| < y). Proof. exact: real_ltr_normlP. Qed. Arguments ltr_normlP {x y}. -Lemma gtr_norm x y : `|x| < y -> x < y. Proof. exact: real_gtr_norm. Qed. +Lemma ltr_normlW x y : `|x| < y -> x < y. Proof. exact: real_ltr_normlW. Qed. -Lemma gtrNnorm x y : `|x| < y -> - y < x. Proof. exact: real_gtrNnorm. Qed. +Lemma ltrNnormlW x y : `|x| < y -> - y < x. Proof. exact: real_ltrNnormlW. Qed. -Lemma ger_norm x y : `|x| <= y -> x <= y. Proof. exact: real_ger_norm. Qed. +Lemma ler_normlW x y : `|x| <= y -> x <= y. Proof. exact: real_ler_normlW. Qed. -Lemma gerNnorm x y : `|x| <= y -> - y <= x. Proof. exact: real_gerNnorm. Qed. +Lemma lerNnormlW x y : `|x| <= y -> - y <= x. Proof. exact: real_lerNnormlW. Qed. Lemma ler_normr x y : (x <= `|y|) = (x <= y) || (x <= - y). -Proof. by rewrite leNgt ltr_norml negb_and -!leNgt orbC ler_oppr. Qed. +Proof. exact: real_ler_normr. Qed. Lemma ltr_normr x y : (x < `|y|) = (x < y) || (x < - y). -Proof. by rewrite ltNge ler_norml negb_and -!ltNge orbC ltr_oppr. Qed. +Proof. exact: real_ltr_normr. Qed. Definition lter_normr := (ler_normr, ltr_normr). Lemma ler_distl x y e : (`|x - y| <= e) = (y - e <= x <= y + e). -Proof. by rewrite lter_norml !lter_sub_addl. Qed. +Proof. exact: real_ler_distl. Qed. Lemma ltr_distl x y e : (`|x - y| < e) = (y - e < x < y + e). -Proof. by rewrite lter_norml !lter_sub_addl. Qed. +Proof. exact: real_ltr_distl. Qed. Definition lter_distl := (ler_distl, ltr_distl). -Lemma ltr_dist_addl x y e : `|x - y| < e -> x < y + e. -Proof. exact: real_ltr_dist_addl. Qed. +Lemma ltr_distl_addr x y e : `|x - y| < e -> x < y + e. +Proof. exact: real_ltr_distl_addr. Qed. -Lemma ler_dist_addl x y e : `|x - y| <= e -> x <= y + e. -Proof. exact: real_ler_dist_addl. Qed. +Lemma ler_distl_addr x y e : `|x - y| <= e -> x <= y + e. +Proof. exact: real_ler_distl_addr. Qed. -Lemma ltr_distr_addl x y e : `|x - y| < e -> y < x + e. -Proof. exact: real_ltr_distr_addl. Qed. +Lemma ltr_distl_addrC x y e : `|x - y| < e -> y < x + e. +Proof. exact: real_ltr_distl_addrC. Qed. -Lemma ler_distr_addl x y e : `|x - y| <= e -> y <= x + e. -Proof. exact: real_ler_distr_addl. Qed. +Lemma ler_distl_addrC x y e : `|x - y| <= e -> y <= x + e. +Proof. exact: real_ler_distl_addrC. Qed. -Lemma ltr_dist_subl x y e : `|x - y| < e -> x - e < y. -Proof. exact: real_ltr_dist_subl. Qed. +Lemma ltr_distl_subl x y e : `|x - y| < e -> x - e < y. +Proof. exact: real_ltr_distl_subl. Qed. -Lemma ler_dist_subl x y e : `|x - y| <= e -> x - e <= y. -Proof. exact: real_ler_dist_subl. Qed. +Lemma ler_distl_subl x y e : `|x - y| <= e -> x - e <= y. +Proof. exact: real_ler_distl_subl. Qed. -Lemma ltr_distr_subr x y e : `|x - y| < e -> y - e < x. -Proof. exact: real_ltr_distr_subr. Qed. +Lemma ltr_distl_sublC x y e : `|x - y| < e -> y - e < x. +Proof. exact: real_ltr_distl_sublC. Qed. -Lemma ler_distr_subr x y e : `|x - y| <= e -> y - e <= x. -Proof. exact: real_ler_distr_subr. Qed. - -Lemma gt_norm_eqF (x y : R) : `|x| < y -> (x == - y = false) * (x == y = false). -Proof. -move=> x1; split; last by rewrite lt_eqF // (le_lt_trans (ler_norm _) x1). -by move: x1; rewrite ltr_norml => /andP[? ?]; rewrite gt_eqF. -Qed. +Lemma ler_distl_subrC x y e : `|x - y| <= e -> y - e <= x. +Proof. exact: real_ler_distl_sublC. Qed. Lemma exprn_even_ge0 n x : ~~ odd n -> 0 <= x ^+ n. Proof. by move=> even_n; rewrite real_exprn_even_ge0 ?num_real. Qed. -- cgit v1.2.3 From 847cc0eab00c004b52195f8d63a763725524fe2f Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 5 Jun 2020 00:49:15 +0900 Subject: fix naming --- mathcomp/algebra/ssrnum.v | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 8184577..95c40cd 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -2924,10 +2924,10 @@ Proof. by move=> ?; rewrite real_ltr_distl // => /andP[]. Qed. Lemma real_ler_distl_addr x y e : x - y \is real -> `|x - y| <= e -> x <= y + e. Proof. by move=> ?; rewrite real_ler_distl // => /andP[]. Qed. -Lemma real_ltr_distl_addrC x y e : x - y \is real -> `|x - y| < e -> y < x + e. +Lemma real_ltr_distlC_addr x y e : x - y \is real -> `|x - y| < e -> y < x + e. Proof. by rewrite realBC (distrC x) => ? /real_ltr_distl_addr; apply. Qed. -Lemma real_ler_distl_addrC x y e : x - y \is real -> `|x - y| <= e -> y <= x + e. +Lemma real_ler_distlC_addr x y e : x - y \is real -> `|x - y| <= e -> y <= x + e. Proof. by rewrite realBC distrC => ? /real_ler_distl_addr; apply. Qed. Lemma real_ltr_distl_subl x y e : x - y \is real -> `|x - y| < e -> x - e < y. @@ -2936,10 +2936,10 @@ Proof. by move/real_ltr_distl_addr; rewrite ltr_sub_addr; apply. Qed. Lemma real_ler_distl_subl x y e : x - y \is real -> `|x - y| <= e -> x - e <= y. Proof. by move/real_ler_distl_addr; rewrite ler_sub_addr; apply. Qed. -Lemma real_ltr_distl_sublC x y e : x - y \is real -> `|x - y| < e -> y - e < x. +Lemma real_ltr_distlC_subl x y e : x - y \is real -> `|x - y| < e -> y - e < x. Proof. by rewrite realBC distrC => ? /real_ltr_distl_subl; apply. Qed. -Lemma real_ler_distl_sublC x y e : x - y \is real -> `|x - y| <= e -> y - e <= x. +Lemma real_ler_distlC_subl x y e : x - y \is real -> `|x - y| <= e -> y - e <= x. Proof. by rewrite realBC distrC => ? /real_ler_distl_subl; apply. Qed. (* GG: pointless duplication }-( *) @@ -3804,11 +3804,11 @@ Proof. exact: real_ltr_distl_addr. Qed. Lemma ler_distl_addr x y e : `|x - y| <= e -> x <= y + e. Proof. exact: real_ler_distl_addr. Qed. -Lemma ltr_distl_addrC x y e : `|x - y| < e -> y < x + e. -Proof. exact: real_ltr_distl_addrC. Qed. +Lemma ltr_distlC_addr x y e : `|x - y| < e -> y < x + e. +Proof. exact: real_ltr_distlC_addr. Qed. -Lemma ler_distl_addrC x y e : `|x - y| <= e -> y <= x + e. -Proof. exact: real_ler_distl_addrC. Qed. +Lemma ler_distlC_addr x y e : `|x - y| <= e -> y <= x + e. +Proof. exact: real_ler_distlC_addr. Qed. Lemma ltr_distl_subl x y e : `|x - y| < e -> x - e < y. Proof. exact: real_ltr_distl_subl. Qed. @@ -3816,11 +3816,11 @@ Proof. exact: real_ltr_distl_subl. Qed. Lemma ler_distl_subl x y e : `|x - y| <= e -> x - e <= y. Proof. exact: real_ler_distl_subl. Qed. -Lemma ltr_distl_sublC x y e : `|x - y| < e -> y - e < x. -Proof. exact: real_ltr_distl_sublC. Qed. +Lemma ltr_distlC_subl x y e : `|x - y| < e -> y - e < x. +Proof. exact: real_ltr_distlC_subl. Qed. -Lemma ler_distl_subrC x y e : `|x - y| <= e -> y - e <= x. -Proof. exact: real_ler_distl_sublC. Qed. +Lemma ler_distlC_subr x y e : `|x - y| <= e -> y - e <= x. +Proof. exact: real_ler_distlC_subl. Qed. Lemma exprn_even_ge0 n x : ~~ odd n -> 0 <= x ^+ n. Proof. by move=> even_n; rewrite real_exprn_even_ge0 ?num_real. Qed. -- cgit v1.2.3