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