proposition: Lemma MeasureDifference : forall {IS : IntegrationSpace} (A B : X (ElemFunc IS) -> Prop) (aInt : IntegrableSet A) (bInt : IntegrableSet B), MeasureSet (IntegrableSetDifference A B aInt bInt) == MeasureSet aInt - MeasureSet (IntegrableSetIntersect A B aInt bInt).
proof: Proof. intros. unfold MeasureSet. rewrite <- IntegralMinus. apply IntegralExtensional. intros. destruct xdg. rewrite (applyXminus (CharacFunc A) (CharacFunc (fun x0 : X (ElemFunc IS) => A x0 /\ B x0))). destruct xdf; simpl. destruct d0. destruct d. destruct a,a0; contradiction. destruct a0; contradiction. destruct d. unfold CRminus. rewrite CRopp_0, CRplus_0_r. reflexivity. destruct a; contradiction. destruct d0. destruct d. unfold CRminus. rewrite CRplus_opp_r. reflexivity. destruct a; contradiction. destruct d. 2: unfold CRminus; rewrite CRplus_opp_r; reflexivity. exfalso. apply n. split. exact a. intro abs. apply n0. split; assumption. Qed.
imports: Logic.ConstructiveEpsilon QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTPositivity