proposition: Lemma Udiv_plus_le : forall x y z, x/z + y/z <= (x+y)/z.
proof: Proof. intros; apply (Ueq_orc 0 z); auto; intros. repeat (rewrite Udiv_by_zero; auto). intros; apply Umult_div_le_left; auto. rewrite Umult_sym; rewrite Udistr_plus_left_le. apply Uplus_le_compat; rewrite Umult_sym; auto. Qed.
imports: ALEA(Utheory)