nitpick

math-comp · Aug 1, 2024 · 626d1e5 · 626d1e5
1 parent 181ec3a
commit 626d1e5
Showing 1 changed file with 0 additions and 2 deletions.
diff --git 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}) :