proposition: Lemma Umult_div_le_left : forall x y z, ~0==y -> x*y<=z -> x <= z/y.
proof: Proof. intros; apply (Ule_total y z); auto; intros. rewrite (Udiv_le_one z); auto. apply Umult_le_simpl_right with y; auto. apply Ole_trans with z; auto. rewrite (Udiv_mult z H); auto. Qed.
imports: ALEA(Utheory)