proposition: Lemma Umult_div_le_right : forall x y z, x <= y*z -> x/z <= y.
proof: Proof. intros; apply (Ueq_orc 0 z); auto; intros. rewrite Udiv_by_zero; auto. apply Umult_le_simpl_right with z; auto. assert (x<=z). apply Ole_trans with (y*z); auto. rewrite (Udiv_mult x H0); auto. Qed.
imports: ALEA(Utheory)