proposition: Lemma IntegrableMinusMaj : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f) (g : PartialFunction (X (ElemFunc IS))) (gInt : IntegrableFunction g), PartialRestriction (XinfiniteSumAbs (IntFn (let (i,_) := IntegrableMinus fInt gInt in i))) (Xminus f g).
proof: Proof. intros. apply IntegrablePlusMaj. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase