proposition: Lemma Umult_inv_plus : forall x y, x * [1-] y + y == x + y * [1-] x.
proof: Proof. intros; apply Oeq_trans with (x * [1-] y + y * ([1-] x + x)). setoid_rewrite (Uinv_opp_left x); auto. assert (H:[1-] x <= [1-] x); auto. rewrite (Udistr_plus_left y ([1-] x) x H). apply Oeq_trans with (x * [1-] y + y * x + y * [1-] x). norm_assoc_right; auto. rewrite (Umult_sym y x). assert (H1:[1-] y <= [1-] y); auto. rewrite <- (Udistr_plus_left x ([1-]y) y H1). setoid_rewrite (Uinv_opp_left y); auto. Qed.
imports: ALEA(Utheory)