proposition: Lemma mult_fin_r_mono : forall alpha beta , alpha < beta -> forall n, alpha * S n < beta * S n.
proof: Proof. induction n; simpl; [assumption|]. apply plus_mono_bi; [ right; assumption | assumption]. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles) ZornsLemma(CountableTypes)