proposition: Lemma Uesp_minus_distr : forall x y z t, (x & y) - (z + t) == (x - z) & (y - t).
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)). setoid_rewrite (Uinv_inv ([1-] y + t)). repeat norm_assoc_right; auto. Qed.
imports: ALEA(Utheory)