proposition: Lemma AP_finite_eq_one : forall n: nat, AP n -> n = 1.
proof: Proof. intro n; case n. - inversion 1. simpl in H0; case (@lt_irrefl zero);auto. - intro n0;case n0; trivial. inversion_clear 1. generalize (H1 (F 1)); intros; absurd (F 1 + F (S (S n1)) = F (S (S n1))). + rewrite <- plus_FF;simpl; intro H2. case (@lt_irrefl (succ (succ (F n1)))). pattern (succ (succ (F n1))) at 2; rewrite <- H2; auto with schutte. + apply H, finite_mono; auto with arith. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)