proposition: Theorem zorns_lemma {A} R {preR: PreOrder R} (chains_have_upper_bounds: ∀ (C: A → Prop), (∀ x y, C x → C y → R x y ∨ R y x) → ∃ m, ∀ x, C x → R x m): ∃ m: A, ∀ x, R m x → R x m.
proof: Proof. apply Private.zorns_lemma with (eqA := Private.default_eq R) (ltA := Private.default_lt R); auto; [reflexivity..|]. intros [C Cset] [total _]; cbn in *. apply chains_have_upper_bounds, total. Qed.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)