proposition: Lemma Uinv_bary : forall x y : U, [1-] (a * x + b * y) == a * [1-] x + b * [1-] y + [1-] (a + b).
proof: Proof. intros. apply Uplus_eq_simpl_left with (a * x); auto. apply Uinv_le_perm_right. setoid_rewrite (Udistr_inv_left a x). repeat norm_assoc_right. apply Uplus_le_compat_right. apply Ole_trans with (b + [1-] (a + b)); auto. apply Ole_trans with ([1-] (a + b) + b); auto. apply Oeq_trans with ([1-] (b * y)). apply Oeq_trans with ([1-] (a * x + b * y) + a * x); auto. setoid_rewrite (Udistr_inv_left b y); auto. apply Oeq_trans with ((a * x + a * [1-] x) + b * [1-] y + [1-] (a + b)). assert (x <= ([1-] ([1-] x))); auto. rewrite <- (Udistr_plus_left a _ _ H); auto. rewrite (Uinv_opp_right x). rewrite (Umult_one_right a). apply Oeq_trans with (b * [1-] y + ([1-] (a + b) + a)). assert (b <= [1-] a); auto. rewrite (Uinv_plus_left _ _ H0); auto. rewrite (Uplus_sym a (b * [1-] y)); auto. apply Oeq_trans with (b * [1-] y + (a + [1-] (a + b))); auto. apply Oeq_trans with (((a * x + a * [1-] x) + (b * [1-] y + [1-] (a + b)))); auto. apply Oeq_trans with (((a * x + (a * [1-] x + (b * [1-] y + [1-] (a + b)))))); auto. Qed.
imports: ALEA(Utheory)