proposition: Lemma MeasureDifferenceIncluded : forall {IS : IntegrationSpace} (A B : X (ElemFunc IS) -> Prop) (aInt : IntegrableSet A) (bInt : IntegrableSet B), (forall x:X (ElemFunc IS), B x -> A x) -> MeasureSet (IntegrableSetDifference A B aInt bInt) == MeasureSet aInt - MeasureSet bInt.
proof: Proof. intros. rewrite MeasureDifference. apply CRplus_morph. reflexivity. apply CRopp_morph. apply IntegralExtensional. intros. simpl. destruct xdf, xdg. reflexivity. 3: reflexivity. destruct a. contradiction. exfalso. apply n. split. apply H, b. exact b. Qed.
imports: Logic.ConstructiveEpsilon QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTPositivity