proposition: Lemma Uinv_half_bary : forall x y : U, [1-] ([1/2] * x + [1/2] * y) == [1/2] * [1-] x + [1/2] * [1-] y.
proof: Proof. intros; rewrite Uinv_bary; auto. rewrite Unth_one_plus; rewrite Uinv_one; auto. Qed.
imports: ALEA(Utheory)