proposition: Lemma least_AP : least_member lt AP 1.
proof: Proof. repeat split. - simpl (F 1). auto with schutte. - intros beta H; assert (beta = zero). { simpl (F 1) in H; apply le_alpha_zero, lt_succ_le_2. assumption. } subst beta; rewrite zero_plus_alpha; reflexivity. - intros x H0; tricho x (F 1) H3. + simpl (F 1) in H3; assert (x = zero). { now apply le_alpha_zero, lt_succ_le_2. } subst x; destruct H0; now case (@lt_irrefl zero). + subst x; now left. + right; auto. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)