proposition: Lemma finite_lt_inv : forall i o, o < F i -> exists j:nat , (j<i)%nat /\ o = F j.
proof: Proof. induction i. - simpl (F 0); intros ; destruct (not_lt_zero H ). - simpl (F (S i));intros o H; destruct (@lt_succ_le_2 o (F i)); auto with schutte. + exists i; split; auto. + destruct (IHi o H0) as [x [H1 H2]]. exists x; case H1;auto with arith. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)