proposition: Lemma of_image : forall f A B, ordering_function f A B -> ordering_function f A (image A f).
proof: Proof. intros f A B O; case O; intros H H0; decompose [and] H0. repeat split;auto. intros; exists a; auto. Qed.
imports: ZornsLemma(CountableTypes)