proposition: Lemma ApplyOutsidePointLeft : forall {I J : IntegrationSpace} (hn : list (@ProdIntegrable I J)) (x : X (ElemFunc I)) (y : X (ElemFunc J)) (xyH : Domain (ProdLFunc hn) (x,y)), Forall (fun fg : ProdIntegrable => ~ prodint_g fg y) hn -> SubsetIntersectFactor hn (ProdIntegrableSubsetLeft hn x y xyH) (ProdIntegrableSubsetRight hn x y xyH) == 0.
proof: Proof. induction hn. - reflexivity. - intros. inversion H. destruct xyH, d. specialize (IHhn x y d0 H3). subst x0. subst l. simpl. destruct d. + destruct d1. contradiction. simpl. rewrite IHhn. apply CRplus_0_l. + simpl. rewrite IHhn. apply CRplus_0_l. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile