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}) :