From 59ca32c5ce0d8086abcf041aa5a32a51efa000fb Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 13 Nov 2024 18:06:39 +0100 Subject: [PATCH] proof simplification --- theories/normedtype.v | 20 ++------------------ 1 file changed, 2 insertions(+), 18 deletions(-) diff --git a/theories/normedtype.v b/theories/normedtype.v index 8d0fc8437..889dc6d1b 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -5345,27 +5345,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",