proposition: Theorem zorns_lemma (all_chains_bounded: ∀ F, well_ordered F → ∃ m, ∀ x, x ∈ F → x ≼ m): ∃ m: A, ∀ x, m ≼ x → x ≼ m.
proof: Proof. destruct (@ProperRelationalChoice _ _ _ _ _ _ bound_relation) as [g [g_sub [g_proper [g_complete g_unique]]]]. { unfold bound_relation. intros [S Swo] [S' S'wo] eqS b b' eqb. change (S ≌ S') in eqS. cbn. setoid_rewrite eqS. now setoid_rewrite eqb. } { intros [S Swo]. unfold bound_relation; cbn. destruct (all_chains_bounded S Swo) as [m m_bound]. destruct (classic (∃ b, ∀ x, x ∈ S → x ≺ b)) as [[b b_bound]|no_strong_bound]. - exists b; split. + intros; apply ltA_spec; auto. + intros _ [ ]%b_bound%irreflexivity. - exists m; tauto. } { destruct (must_have_included_bound (λ S b, ∃ W, g (exist _ S W) b)) as [S [b [Swo [[W bbound] inb]]]]. - intros S b b' [W bbound] [W' b'bound]. eapply g_unique; eauto. eapply g_proper; eauto. now change (S ≌ S). - apply proper_sym_impl_iff_2; [firstorder|apply _|]. intros S S' eqS b b' eqb [W bound]. assert (well_ordered S') as W' by now rewrite <- eqS. exists W'. now revert bound; apply g_proper; [change (S' ≌ S)|]. - intros S Swo. destruct (g_complete (exist _ S Swo)) as [b rel]. eauto. - intros ??? Swo [W [bound _]%g_sub] inx. apply bound; trivial. - intros S b Swo [W [_ strong]%g_sub] strong_bound. apply strong; trivial. - exists b; intros x lb. destruct (classic (x ≼ b)) as [|contra]; trivial. apply g_sub in bbound. destruct bbound as [bound strong]; cbn in strong. apply strong in inb; [contradiction|]. exists x. intros y iny%bound. eapply le_lt_trans; eauto. rewrite ltA_spec; auto. } Qed.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)