proposition: Lemma IntegralOpp : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f), Integral (IntegrableScale f (-(1)) fInt) == - Integral fInt.
proof: Proof. intros. rewrite IntegralScale. rewrite <- CRopp_mult_distr_r, CRmult_1_r. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase