proposition: Lemma ordering_function_monoR : 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. destruct 1 as [H H0 H1 H2]; intros a b H3 H4 H5; tricho a b Ht; auto. - subst b; now destruct (@lt_irrefl (f a)). - destruct (@lt_irrefl (f a)); apply lt_trans with (f b); auto. Qed.
imports: ZornsLemma(CountableTypes)