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