proposition: Lemma range_le : forall A (P:A->Prop) (d:Distr A), range P d -> forall f g, (forall a, P a -> f a <= g a) -> mu d f <= mu d g.
proof: Proof. intros; assert (mu d f - mu d g <= 0). apply Ole_trans with (mu d (fun x => f x - g x)). apply mu_stable_le_minus. apply Oeq_le; apply Oeq_sym; apply H; intros. rewrite Uminus_le_zero; auto. apply Uminus_zero_le; apply Ule_zero_eq; exact H1. Qed.
imports: ALEA(Probas) ALEA(Utheory)