proposition: Lemma Iminus : forall {IS : IntegrationSpace} (f g : PartialFunction (X (ElemFunc IS))) (fL : L (ElemFunc IS) f) (gL : L (ElemFunc IS) g), I IS (Xminus f g) (LminusStable f g fL gL) == I IS f fL - I IS g gL.
proof: Proof. intros. unfold Xminus. unfold LminusStable. rewrite Iadditive. apply CRplus_morph. reflexivity. rewrite Ihomogeneous. rewrite <- CRopp_mult_distr_l, CRmult_1_l. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions