proposition: Lemma IntegralMinus : forall {IS : IntegrationSpace} (f g : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f) (gInt : IntegrableFunction g), Integral (IntegrableMinus fInt gInt) == Integral fInt - Integral gInt.
proof: Proof. intros. unfold Xminus. unfold IntegrableMinus. rewrite IntegralPlus. rewrite IntegralScale. apply CRplus_morph. reflexivity. rewrite <- CRopp_mult_distr_r, CRmult_1_r. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase