proposition: Lemma wo_transitive: forall R:relation T, well_order R -> transitive R.
proof: Proof. intros. unfold transitive. intros. case (wo_total_strict_order R H x z). { trivial. } intro. case H2. - intro. rewrite H3 in H0. pose proof (wo_antisym R H y z). contradict H0. auto. - intro. assert (forall a:T, Acc R a -> a <> x /\ a <> y /\ a <> z). { intros. induction H4. intuition; subst. - specialize (H5 z H3). tauto. - specialize (H5 z H0). tauto. - specialize (H5 y H1). tauto. - specialize (H5 z H3). tauto. - specialize (H5 x H0). tauto. - pose proof (H5 y H1). tauto. } pose proof (wo_well_founded R H). unfold well_founded in H5. pose proof (H4 x (H5 x)). tauto. Qed.
imports: Coq(Classical Description FunctionalExtensionality ProofIrrelevance) ZornsLemma(Classical_Wf EnsemblesSpec Relation_Definitions_Implicit ZornsLemma)