proposition: Lemma ApplyProdLFuncDisjointHead : forall {I J : IntegrationSpace} (l : list ProdIntegrable) (a : @ProdIntegrable I J) (x : X (ElemFunc I)) (y : X (ElemFunc J)) (xyL : Domain (ProdLFunc l) (x,y)), ProdIntegrableSimple (a :: l) -> prodint_f a x -> prodint_g a y -> partialApply _ (x,y) xyL == 0.
proof: Proof. induction l. - intros. reflexivity. - intros. simpl. destruct xyL, d. simpl. assert (ProdIntegrableSimple (a0 :: l)) as simple0. { destruct H, H. split. exact H. inversion H2. exact H7. } destruct d. + destruct d1. exfalso. simpl in p, p0. destruct H. inversion H2. apply (H5 x y). repeat split; assumption. rewrite CRmult_0_r, CRplus_0_l. apply (IHl a0). exact simple0. exact H0. exact H1. + rewrite CRmult_0_r, CRmult_0_l, CRplus_0_l. apply (IHl a0). exact simple0. exact H0. exact H1. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile