proposition: Lemma Uminus_distr_right : forall x y z, x * (y - z) == (x * y) - (x * z).
proof: Proof. intros; setoid_rewrite (Umult_sym x y). setoid_rewrite (Umult_sym x z). setoid_rewrite (Umult_sym x (y - z)); auto. Qed.
imports: ALEA(Utheory)