From 626d1e5aac000b0e464f5c8f82afee8ad3b5b55f Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Thu, 1 Aug 2024 12:50:13 +0900
Subject: [PATCH] nitpick

---
 classical/wochoice.v | 2 --
 1 file changed, 2 deletions(-)

diff --git a/classical/wochoice.v b/classical/wochoice.v
index f5bb22296b..d291241465 100644
--- a/classical/wochoice.v
+++ b/classical/wochoice.v
@@ -131,8 +131,6 @@ move=> z [_ Uz] /andP[Rxy Ryx]; have /and3P[xy_x xy_y _] := all_mem [:: x; y].
 by rewrite -(Uz x) ?(Uz y); split=> //; apply/allP; rewrite /= (Rxy, Ryx) Rxx.
 Qed.
 
-(******************************************************************************)
-
 Section Zorn.
 
 Lemma Zorn's_lemma (T : eqType) (R : rel T) (S : {pred T}) :