proposition: Lemma Umult_div_le : forall x y, y * (x / y) <= x.
proof: Proof. intros; apply (Ueq_orc 0 y); auto; intros. apply Ole_trans with (0 * (x/y)); auto. rewrite Umult_zero_left; auto. intros; apply (Ule_total x y); auto; intros. rewrite Udiv_le_one; auto. rewrite Umult_one_right; auto. Qed.
imports: ALEA(Utheory)