proposition: Lemma Uesp_zero_one_mult_right : forall x y, orc (y == 0) (y == 1) -> x & y == x * y.
proof: Proof. intros; apply H; intros; auto. rewrite H0; rewrite Uesp_zero_right; auto. rewrite H0; rewrite Uesp_one_right; auto. Qed.
imports: ALEA(Utheory)