proposition: Lemma wo_antisym: forall R:relation T, well_order R -> (forall x y:T, R x y -> ~ R y x).
proof: Proof. intuition. assert (forall z:T, Acc R z -> z <> x /\ z <> y). intros. induction H2. intuition. rewrite H4 in H3. pose proof (H3 y H1). tauto. rewrite H4 in H3. pose proof (H3 x H0). tauto. pose proof (wo_well_founded R H). unfold well_founded in H3. pose proof (H2 x (H3 x)). tauto. Qed.
imports: Relation_Definitions Relation_Definitions_Implicit Classical_Wf Description FunctionalExtensionality Classical ZornsLemma ProofIrrelevance EnsemblesSpec