proposition: Lemma IntegralDistance_sym : forall { IS : IntegrationSpace } (f g : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f) (gInt : IntegrableFunction g), IntegralDistance fInt gInt == IntegralDistance gInt fInt.
proof: Proof. intros. apply IntegralExtensional. intros. do 2 rewrite applyXabs. destruct xdf, xdg. rewrite (applyXminus f g), (applyXminus g f). rewrite CRabs_minus_sym. apply CRabs_morph, CRplus_morph. apply DomainProp. apply CRopp_morph. apply DomainProp. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase