proposition: Theorem well_ordering_from_zorns_lemma (zl: ∀ A R preR chub, @ZornsLemma A R preR chub) {A} (eqA: relation A) {equA: Equivalence eqA}: ∃ ltA, well_order eqA ltA.
proof: Proof. pose proof (zl _ (continues eqA) (continues_preorder eqA)) as zl'. unfold ZornsLemma in zl'. destruct zl' as [o omax]. - intros C Cchain. exists (exist _ (union_S eqA C, union_R eqA C) (union_good eqA C Cchain): order eqA). intros o ino. split; cbn. + intros x inx; exists o; auto. + intros ?? [o' [ino' inx]] iny [o'' [ino'' rel']]. destruct (Cchain o' o ino' ino) as [[ ]|[sub cl co]]; auto. pose proof (sub _ iny) as iny'. destruct (Cchain o'' o' ino'' ino') as [[sub' cl' co']|[sub' cl' co']]. * destruct (o''.good) as [_ _ _ _ correct _]. destruct (correct _ _ rel') as [inx'' iny'']. rewrite co' in rel'; auto. destruct (o'.good); eauto. * rewrite <- co' in rel'; trivial. destruct (o'.good); eauto. + intros ?? inx iny; split; [exists o; auto|]. intros [o' [ino' rel]]. destruct (Cchain _ _ ino ino') as [[sub cl co]|[sub cl co]]; [now apply co|]. destruct (o'.good) as [_ _ _ _ correct _]. destruct (correct _ _ rel). now apply co. - exists (o.R). pose proof (maximal_continuation_total eqA o omax) as total. clear omax. destruct o as [[S R] [sproper strict wf rproper correct complete]]. now split. Qed.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)