proposition: Lemma IabsMinusMaj : forall (IS : IntegrationSpace) (f g : PartialFunction (X (ElemFunc IS))) (fL : L (ElemFunc IS) f) (gL : L (ElemFunc IS) g), - Iabs f fL + Iabs g gL <= Iabs (Xminus f g) (LminusStable f g fL gL).
proof: Proof. intros. rewrite CRplus_comm. unfold Iabs. pose proof (@Iminus IS). unfold CRminus in H. rewrite <- H. clear H. apply INonDecreasing. intros. destruct y. rewrite applyXabs. rewrite (applyXminus f g). destruct xF. rewrite (applyXminus (Xabs g) (Xabs f)). unfold Xabs, Xop, partialApply. destruct f,g. rewrite (DomainProp0 x d0 d1), (DomainProp x d2 d). rewrite CRabs_minus_sym. apply CRabs_triang_inv. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions