proposition: Lemma Nmult_def_lt : forall n x, n */ x <1 -> Nmult_def n x.
proof: Proof. red; destruct n; intros; auto. apply (Ule_total x ([1/]1+n)); intros; auto. case H. apply Ole_trans with (S n */ [1/]1+n); auto. Qed.
imports: ALEA(Utheory)