proposition: Theorem well_orderable: exists R:relation T, well_order R.
proof: Proof. assert (exists WO:partial_WO, premaximal partial_WO_ord WO). { apply ZornsLemmaForPreorders. - exact partial_WO_preord. - intros. exists (partial_WO_chain_ub S H). exact (partial_WO_chain_ub_correct S H). } destruct H as [WO]. exists (pwo_R WO). constructor. - assert (forall x:T, In (pwo_S WO) x). { rewrite premaximal_partial_WO_is_full. - intro. constructor. - assumption. } assert (forall a:{x:T | In (pwo_S WO) x}, Acc (pwo_R WO) (proj1_sig a)). { intro. pose proof (wo_well_founded (pwo_wo WO)). induction (H1 a). destruct x. simpl. unfold restriction_relation in H3; simpl in H3. constructor. intros. apply H3 with (y := exist _ y (H0 y)). assumption. } red; intro. apply H1 with (a := exist _ a (H0 a)). - red; intros. assert (forall x:T, In (pwo_S WO) x). { rewrite premaximal_partial_WO_is_full; intro. - constructor. - apply H. } case (wo_total_strict_order (pwo_wo WO) (exist _ x (H0 x)) (exist _ y (H0 y))). { unfold restriction_relation; tauto. } intro. case H1. + intro. right; left. injection H2. trivial. + unfold restriction_relation; tauto. Qed.
imports: Coq(Classical Description FunctionalExtensionality ProofIrrelevance) ZornsLemma(Classical_Wf EnsemblesSpec Relation_Definitions_Implicit ZornsLemma)