proposition: Lemma Uminus_esp_simpl_left : forall x y, [1-]x <= y -> x - (x & y) == [1-]y.
proof: Proof. unfold Uesp,Uminus; intros. apply Uinv_eq_compat. rewrite (Uplus_sym ([1-]x)). rewrite Uinv_plus_left; auto. Qed.
imports: ALEA(Utheory)