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