proposition: Lemma omega_second_AP : least_member lt (fun alpha => 1 < alpha /\ In AP alpha) omega.
proof: Proof. Proof with auto with schutte. split. - split. + apply finite_lt_omega. + apply AP_omega. - intros x H0; case (@trichotomy x omega). + intro H1; case (lt_omega_finite H1). intros; subst x. destruct H0 as [H2 H3]; generalize (AP_finite_eq_one _ H3). intro;subst x0;now destruct (@lt_irrefl (F 1)). + red; intuition. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)