proposition: Lemma MeasureNonDecreasing : forall {IS : IntegrationSpace} (A B : X (ElemFunc IS) -> Prop) (aInt : IntegrableSet A) (bInt : IntegrableSet B), (forall x : X (ElemFunc IS), A x -> B x) -> MeasureSet aInt <= MeasureSet bInt.
proof: Proof. intros. apply IntegralNonDecreasing. intros x xdf xdg. simpl. destruct xdf, xdg. apply CRle_refl. exfalso. specialize (H x a). contradiction. apply CRlt_asym, CRzero_lt_one. apply CRle_refl. Qed.
imports: Logic.ConstructiveEpsilon QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTPositivity