proposition: Lemma not_is_succ_zero : ~ is_succ zero.
proof: Proof. intros (b, Hb); apply (succ_zero_diff b); now symmetry. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)