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. rewrite H2 in H5. pose proof (H5 z H3). tauto. rewrite H2 in H5. pose proof (H5 x H0). tauto. rewrite H2 in H5. pose proof (H5 y H1). tauto. rewrite H2 in H5. pose proof (H5 z H3). tauto. rewrite H2 in H5. pose proof (H5 x H0). tauto. rewrite H2 in H5. 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: Relation_Definitions Relation_Definitions_Implicit Classical_Wf Description FunctionalExtensionality Classical ZornsLemma ProofIrrelevance EnsemblesSpec