proposition: Lemma Random_carac : forall (P:nat -> Prop)(Pdec : dec P)(n:nat), mu (Random n) (carac Pdec) == (nb_elts Pdec (S n)) */ [1/]1+n.
proof: Proof. simpl mu. unfold random,fnth; intros. elim (S n); simpl; intros;auto. rewrite H; unfold carac;case (Pdec n0); Usimpl; auto. Qed.
imports: ALEA(Utheory) ALEA(Sets)