proposition: Lemma Ordering_bijection : forall f A B, ordering_function f A B -> fun_bijection A B f.
proof: Proof. destruct 1 as [H H0 H1 H2]. split;red;auto; intros. tricho a a' H7; trivial. - specialize (H2 _ _ H3 H4 H7); rewrite H5 in H2; destruct (lt_irrefl H2). - specialize (H2 _ _ H4 H3 H7); rewrite H5 in H2; destruct (lt_irrefl H2). Qed.
imports: ZornsLemma(CountableTypes)