proposition: Corollary well_ordering_theorem {A} (eqA: relation A) {equA: Equivalence eqA}: ∃ ltA, well_order eqA ltA.
proof: Proof. apply well_ordering_from_zorns_lemma; trivial. intros; apply zorns_lemma; trivial. Qed.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)