proposition: Lemma admissible_le_fix : continuous (D1:=A-O-> cDistr B) (D2:=A-O->cDistr B) F -> admissible (fun f => f <= Mfix F).
proof: Proof. split; intros. auto. apply Ole_trans with (F (Mfix F)). auto. intro x; rewrite Mfix_eq; auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)