proposition: Lemma mult_Sn_mono2 : forall a, zero < a -> forall n p, (n < p)%nat -> a * S n < a * S p.
proof: Proof. Proof with auto with schutte. intros a Ha; induction 1. - simpl; intros; pattern ( mult_Sn a n) at 1; rewrite <- alpha_plus_zero ... + apply plus_mono_r ... - simpl;apply lt_trans with (mult_Sn a m);auto. pattern (mult_Sn a m) at 1; rewrite <- alpha_plus_zero. apply plus_mono_r ... Qed.
imports: Coq(Arith Logic.Epsilon Ensembles) ZornsLemma(CountableTypes)