proposition: Lemma Uesp_minus_distr_left : forall x y z, (x & y) - z == (x - z) & y.
proof: Proof. unfold Uesp, Uminus; intros. apply Uinv_eq_compat. setoid_rewrite (Uinv_inv ([1-] x + [1-] y)). setoid_rewrite (Uinv_inv (([1-] x) + z)). repeat norm_assoc_right; auto. Qed.
imports: ALEA(Utheory)