proposition: Lemma Uinv_mean : forall x y, [1-](mean x y) == mean ([1-]x) ([1-]y).
proof: Proof. unfold mean; intros. repeat rewrite Umult_inv_minus. apply Oeq_trans with ([1/2]+[1/2] - ([1/2] * x + [1/2]*y)). rewrite Unth_one_plus; auto. rewrite <- Uminus_assoc_left. rewrite <- Uminus_plus_perm; auto. rewrite <- Uplus_minus_assoc_right; trivial. apply Uinv_le_perm_right. rewrite <- Unth_one; auto. Qed.
imports: ALEA(Utheory)