diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 4 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 24 |
2 files changed, 14 insertions, 14 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index a5fae21..20594ab 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -12,8 +12,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - in `ssrnum.v`, new lemmas: + `(real_)ltr_normlW`, `(real_)ltrNnormlW`, `(real_)ler_normlW`, `(real_)lerNnormlW` - + `(real_)ltr_distl_addr`, `(real_)ler_distl_addr`, `(real_)ltr_distl_addrC`, `(real_)ler_distl_addrC`, - `(real_)ltr_distl_subl`, `(real_)ler_distl_subl`, `(real_)ltr_distl_sublC`, `(real_)ler_distl_sublC` + + `(real_)ltr_distl_addr`, `(real_)ler_distl_addr`, `(real_)ltr_distlC_addr`, `(real_)ler_distlC_addr`, + `(real_)ltr_distl_subl`, `(real_)ler_distl_subl`, `(real_)ltr_distlC_subl`, `(real_)ler_distlC_subl` ### Changed 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. |