proposition: Lemma U1min_S : forall n, U1min (S n) == [1/2]*(U1min n) + [1/2].
proof: Proof. intros; unfold U1min at 2,pmin. rewrite (Uminus_distr_right [1/2] 1 ([1/2]^n)). rewrite Umult_one_right. rewrite Uminus_plus_perm; auto. rewrite Unth_one_plus; auto. Qed.
imports: ALEA(Utheory)