proposition: Lemma mult_fin_r_one : forall n, (F 1) * S n = F (S n).
proof: Proof. induction n. - trivial. - simpl in *; rewrite IHn; rewrite plus_of_succ. rewrite alpha_plus_zero;auto with schutte. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles) ZornsLemma(CountableTypes)