proposition: Lemma Udistr_plus_left_le : forall x y z : U, x * (y + z) <= x * y + x * z.
proof: Proof. intros; apply (Ule_total y ([1-]z)); intros; auto. apply Ole_trans with (x * ([1-]z+z)). rewrite Uinv_opp_left; auto. rewrite Udistr_plus_left; auto. Qed.
imports: ALEA(Utheory)