proposition: Lemma Random_le : forall n k, mu (Random n) (carac_le k) == (S k) */ [1/]1+n.
proof: Proof. intros; apply Oeq_trans with (mu (Random n) (carac_lt (S k))); auto. apply (mu_stable_eq (Random n)); auto. unfold carac_le,carac_lt. simpl; apply ford_eq_intro; intro x. apply carac_eq_compat; intuition. Qed.
imports: ALEA(Utheory) ALEA(Sets)