proposition: Lemma Uminus_distr_left : forall x y z, (x - y) * z == (x * z) - (y * z).
proof: Proof. intros; apply (Ule_total x y); intros; auto. rewrite (Uminus_le_zero x y); trivial. rewrite (Umult_zero_left z). assert (x * z <= y * z); auto. rewrite (Uminus_le_zero _ _ H0); auto. unfold Uminus; intros; auto. apply Uplus_eq_simpl_right with (y * z); auto. assert ([1-] ([1-] x + y) <= [1-] y); auto. rewrite <- (Udistr_plus_right _ _ z H0); auto. assert (y <= [1-] ([1-] x)); auto. rewrite (Uinv_plus_right _ _ H1). rewrite (Uinv_inv x); auto. Qed.
imports: ALEA(Utheory)