From 881be66f1d5f2b40d47b110d5453a33f69ca2f1f Mon Sep 17 00:00:00 2001
From: zstone <zstonex@gmail.com>
Date: Wed, 2 Oct 2024 08:56:37 -0400
Subject: [PATCH] removing troublesome lemma

---
 CHANGELOG_UNRELEASED.md      |  3 +--
 classical/classical_orders.v | 19 -------------------
 2 files changed, 1 insertion(+), 21 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 4c785bf7a..8924b1821 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -37,8 +37,7 @@
     `big_lexi_le_reflexive`, `big_lexi_le_anti`, `big_lexi_le_trans`,
     `big_lexi_le_total`, `start_with_prefix`, `leEbig_lexi_order`,
     `big_lexi_order_prefix_lt`, `big_lexi_order_prefix_gt`,
-    `big_lexi_order_between`, `big_lexi_order_interval_prefix`, and
-    `big_lexi_order_prefix_closed_itv`.
+    `big_lexi_order_between`, and `big_lexi_order_interval_prefix`.
 
 ### Changed
 
diff --git a/classical/classical_orders.v b/classical/classical_orders.v
index b79f4f7b3..431026c59 100644
--- a/classical/classical_orders.v
+++ b/classical/classical_orders.v
@@ -356,22 +356,3 @@ move: i; case=> [][[]l|[]] [[]r|[]] [][]; rewrite ?in_itv /= ?andbT.
 by move=> _; exists 0 => ? ?; rewrite set_itvE.
 Qed.
 End big_lexi_intervals.
-
-(** TODO: generalize to tbOrderType when that's available in mathcomp *)
-Lemma big_lexi_order_prefix_closed_itv {d} {K : nat -> finOrderType d} n
-  (x : big_lexi_order K) :
-  same_prefix n x = `[
-    (start_with n x (fun=>\bot):big_lexi_order K)%O,
-    (start_with n x (fun=>\top))%O].
-Proof.
-rewrite eqEsubset; split=> [z pfxz|z]; first last.
-  rewrite set_itvE /= => xbt; apply: same_prefix_trans.
-    exact: (start_with_prefix _ (fun=> \bot)%O).
-  apply/same_prefix_sym/(big_lexi_order_between xbt).
-  apply: same_prefix_trans (start_with_prefix _ _).
-  exact/same_prefix_sym/start_with_prefix.
-rewrite set_itvE /= !leEbig_lexi_order; apply/andP; split;
-  case E : (first_diff _ _) => [m|] //; rewrite /start_with /=.
-- by case: ifPn => [/pfxz -> //|]; rewrite le0x.
-- by case: ifPn => [/pfxz -> //|]; rewrite lex1.
-Qed.