proposition: Lemma pmin_esp_S : forall p n, pmin (p & p) n == pmin p (S n) & pmin p (S n).
proof: Proof. unfold pmin at 1; intros. rewrite (half_exp n). rewrite (Uesp_minus_distr p p ([1/2]^(S n)) ([1/2]^(S n))); auto. Qed.
imports: ALEA(Utheory)