proposition: Lemma AP_one : In AP 1.
proof: Proof. Proof with auto with schutte. split. - simpl (F 1) ... - simpl (F 1); intros beta H. assert (H0: beta <= zero). { apply lt_succ_le_2 ... } rewrite (le_alpha_zero H0), zero_plus_alpha... Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)