proposition: Theorem Non_denum : ~ Countable ordinal.
proof: Proof. red; intro H; case (AX3 H); auto. intros x H0; case (@lt_irrefl x);apply H0; split. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)