proposition: Lemma Umult_zero_left : forall x, 0 * x == 0.
proof: Proof. intros; apply Uinv_simpl. setoid_rewrite (Udistr_inv_right 0 x); auto. setoid_rewrite Uinv_zero. setoid_rewrite (Umult_one_left x); auto. Qed.
imports: ALEA(Utheory)