proposition: Lemma DomainProdLFuncInc : forall {I J : IntegrationSpace} (hn : list (@ProdIntegrable I J)) (x : X (ElemFunc I)) (y : X (ElemFunc J)) (xyS : Domain (ProdLFunc hn) (x,y)) (n : nat), lt n (length hn) -> Domain (ProdIntegrableFunc (nth n hn (ProdIntegrableZero I J))) (x,y).
proof: Proof. induction hn. - intros. exfalso; inversion H. - intros. simpl in H. destruct n. + apply xyS. + apply le_S_n in H. simpl. apply (IHhn x y). apply xyS. exact H. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile