proposition: Lemma le_a_mult_Sn_a : forall alpha n, ordinal alpha -> alpha <= alpha * S n.
proof: Proof. intros alpha n H; case n. - simpl;auto with schutte. - intros;simpl;apply le_plus_r;auto with schutte. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles) ZornsLemma(CountableTypes)