proposition: Lemma succ_zero_diff (alpha : Ord): succ alpha <> zero.
proof: Proof. intros H; destruct (@not_lt_zero alpha). rewrite <- H; auto with schutte. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)