proposition: Lemma finite_not_limit (i: nat): ~ is_limit i.
proof: Proof. destruct i. - simpl; apply not_is_limit_zero. - simpl. intros [_ H0]; apply H0; now exists (F i). Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)