proposition: Lemma segment_the_ordering_segment : segment (the_ordering_segment B).
proof: Proof. unfold the_ordering_segment. apply iota_ind. apply ordering_segment_ex_unique. destruct 1. destruct H. now destruct H. Qed.
imports: ZornsLemma(CountableTypes)