proposition: Lemma mult_Sn_mono3 : forall alpha, zero < alpha -> forall n p, (n < p)%nat -> alpha * S n + alpha <= alpha * S p.
proof: Proof. Proof with auto with schutte. intros a Ha; induction 1 . - simpl; apply eq_le ... - simpl; apply plus_mono_weak_l. apply lt_le; apply mult_Sn_mono2 ... Qed.
imports: Coq(Arith Logic.Epsilon Ensembles) ZornsLemma(CountableTypes)