proposition: Lemma countable_not_Unbounded : forall X, Countable X -> not (Unbounded X).
proof: Proof. red;intros; apply Unbounded_not_countable with X;auto. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)