diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 3bb41568dc..8fd6ccd7f7 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -51,6 +51,8 @@
 
 - in `charge.v`:
   + definition `copp`, lemma `cscaleN1`
+- in `classical_orders.v`:
+  + lemma `big_lexi_order_prefix_closed_itv`
 
 ### Changed
 
diff --git a/classical/classical_orders.v b/classical/classical_orders.v
index 431026c590..bd82a8206c 100644
--- a/classical/classical_orders.v
+++ b/classical/classical_orders.v
@@ -355,4 +355,23 @@ move: i; case=> [][[]l|[]] [[]r|[]] [][]; rewrite ?in_itv /= ?andbT.
   by apply: (big_lexi_order_prefix_gt xr E2) => w wm; exact/esym/xppfx.
 by move=> _; exists 0 => ? ?; rewrite set_itvE.
 Qed.
+
 End big_lexi_intervals.
+
+Lemma big_lexi_order_prefix_closed_itv {d} {K : nat -> tbOrderType d} n
+  (x : big_lexi_order K) :
+  same_prefix n x = `[
+    (@start_with K 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.