proposition: Theorem ordering_le : forall f A B, ordering_function f A B -> forall alpha, In A alpha -> alpha <= f alpha.
proof: Proof. Proof with auto with schutte. intros f A B H alpha H0; generalize H0; pattern alpha; apply transfinite_induction. - clear alpha H0; destruct H as [H1 H2 H3 H4]. unfold progressive; intros alpha H6 H7 . tricho alpha (f alpha) H' ... + assert (f (f alpha) < f alpha). { apply H4. - eapply segment_lt;eauto with schutte. - unfold In;auto. - unfold In;auto. } case (le_not_gt (a:= f alpha)(b:=f (f alpha)));auto. apply H6; eauto with schutte. Qed.
imports: ZornsLemma(CountableTypes)