proposition: Lemma pmin_plus_eq : forall p n, p <= [1/2] -> pmin p (S n) == [1/2] * (pmin (p + p) n).
proof: Proof. intros; unfold pmin at 2. setoid_rewrite (Uminus_distr_right [1/2] (p + p) ([1/2]^n)). setoid_rewrite (half_twice _ H); auto. Qed.
imports: ALEA(Utheory)