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: Relation_Definitions Relation_Definitions_Implicit Classical_Wf Description FunctionalExtensionality Classical ZornsLemma ProofIrrelevance EnsemblesSpec