proposition: Lemma ord_ok : ordering_function (ord B) (the_ordering_segment B) B.
proof: Proof. pattern (ord B); apply epsilon_spec. pattern (the_ordering_segment B); apply iota_spec, ordering_segment_ex_unique. Qed.
imports: ZornsLemma(CountableTypes)