proposition: Lemma MeasureDifferenceInvolutive : forall {IS : IntegrationSpace} (A B : X (ElemFunc IS) -> Prop) (aInt : IntegrableSet A) (bInt : IntegrableSet B), MeasureSet (IntegrableSetDifference A _ aInt (IntegrableSetDifference A B aInt bInt)) == MeasureSet (IntegrableSetIntersect A B aInt bInt).
proof: Proof. intros. apply IntegralExtensional. intros. destruct xdf,xdg; simpl. reflexivity. exfalso. destruct a. apply H0. split. exact H. intro abs. apply n. split; assumption. exfalso. apply n. split. apply a. intro abs. destruct a, abs; contradiction. reflexivity. Qed.
imports: Logic.ConstructiveEpsilon QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTPositivity