proposition: Lemma Random_lt : forall n k, mu (Random n) (carac_lt k) == k */ [1/]1+n.
proof: Proof. unfold carac_lt; intros; rewrite Random_carac. case (le_ge_dec k (S n)); intros. rewrite nb_elts_lt_le; auto. rewrite nb_elts_lt_ge; auto. apply Ole_antisym; auto. apply Ole_trans with 1; auto. Qed.
imports: ALEA(Utheory) ALEA(Sets)