From 11d5cf62c8ee39d9e30bfb3483ed2a03c4201fbc Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Sun, 17 Nov 2024 17:03:40 +0100 Subject: [PATCH] proof simplification (#1393) --- theories/normedtype.v | 20 ++------------------ 1 file changed, 2 insertions(+), 18 deletions(-) diff --git a/theories/normedtype.v b/theories/normedtype.v index 839e7edbc..bf18d7bcd 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -5428,27 +5428,11 @@ Proof. exact: interval_open. Qed. Lemma near_in_itvoy : {in `]a, +oo[, forall y, \forall z \near y, z \in `]a, +oo[}. -Proof. -move=> x ax. -near=> z. -suff : z \in `]a, +oo[%classic by rewrite inE. -near: z. -rewrite near_nbhs. -apply: (@open_in_nearW _ _ `]a, +oo[%classic) => //. -by rewrite inE. -Unshelve. end_near. Qed. +Proof. exact: interval_open. Qed. Lemma near_in_itvNyo : {in `]-oo, b[, forall y, \forall z \near y, z \in `]-oo, b[}. -Proof. -move=> x xb. -near=> z. -suff : z \in `]-oo, b[%classic by rewrite inE. -near: z. -rewrite near_nbhs. -apply: (@open_in_nearW _ _ `]-oo, b[%classic) => //. -by rewrite inE/=. -Unshelve. end_near. Qed. +Proof. exact: interval_open. Qed. End near_in_itv. #[deprecated(since="mathcomp-analysis 1.7.0",