proposition: Lemma ordering_function_mono (f : Ord -> Ord) (A B: Ensemble Ord) : ordering_function f A B -> forall alpha beta, In A alpha -> In A beta -> alpha < beta -> f alpha < f beta.
proof: Proof. now destruct 1. Qed.
imports: ZornsLemma(CountableTypes)