Fixpoint choose A (l : list A) : distr A :=
  match l with
    | nil => distr_null A
    | cons hd tl => Mchoice ([1/](length l)) (Munit hd) (choose tl)
  end.

Lemma choose_uniform : forall A (d : A) (l : list A) f,
  mu (choose l) f == sigma (fun i => ([1/](length l)) * f (nth i l d)) (length l).

Lemma In_nth : forall A (x:A) l, In x l -> exists i, (i < length l)%nat /\ nth i l x = x.

Lemma choose_le_Nnth :
  forall A (l:list A) x f alpha,
    In x l ->
    alpha <= f x ->
    [1/](length l) * alpha <= mu (choose l) f.

Fixpoint lrange n := match n with
  | O => cons O nil
  | S m => cons (S m) (lrange m)
end.

Lemma range_len : forall n, length (lrange n) = S n.

Lemma leq_in_range : forall n x, (x<=n)%nat -> In x (lrange n).