proposition: Lemma Uplus_div_inv : forall x y z, x+y <= z -> x<=[1-]y -> x/z <= [1-](y/z).
proof: Proof. intros; apply (Ueq_orc 0 z); auto; intros. repeat (rewrite Udiv_by_zero; auto). apply Umult_div_le_right; auto. apply Uplus_le_simpl_right with ([1-]z). apply Uinv_le_compat; apply Ole_trans with (x+y); auto. rewrite <- Udistr_inv_right. rewrite Udiv_mult; auto. apply Ole_trans with (x+[1-](x+y)); auto. rewrite Uplus_sym; rewrite Uinv_plus_left; auto. apply Ole_trans with (x+y); auto. Qed.
imports: ALEA(Utheory)