proposition: Lemma ordering_function_mono_weakR : forall f A B, ordering_function f A B -> forall a b, In A a -> In A b -> f a <= f b -> a <= b.
proof: Proof. Proof with auto with schutte. intros f A B H a b H0 H1 H2. case H; intros H3 H4 H5 H6. destruct H2 as [H2 | H2]. case (Ordering_bijection H). intros H10 H11 H12 ; specialize (H12 a b H0 H1 )... - right; eapply ordering_function_monoR; eauto. Qed.
imports: ZornsLemma(CountableTypes)