proposition: Lemma Umult_inv_minus : forall x y, x * [1-]y == x - (x * y).
proof: Proof. unfold Uminus; intros. apply Uplus_eq_simpl_right with (x * y). rewrite Udistr_inv_left. rewrite Uinv_inv; auto. rewrite Uinv_inv; auto. rewrite <- Udistr_plus_left; auto. rewrite Uinv_opp_left. rewrite Umult_one_right. rewrite Uinv_plus_right; auto. Qed.
imports: ALEA(Utheory)