proposition: Lemma ProdIntegrableSubsetLeft_length : forall {I J : IntegrationSpace} (hn : list (@ProdIntegrable I J)) (x : X (ElemFunc I)) (y : X (ElemFunc J)) (xyH : Domain (ProdLFunc hn) (x,y)), length (ProdIntegrableSubsetLeft hn x y xyH) = length hn.
proof: Proof. induction hn. - reflexivity. - intros. simpl. destruct xyH, d. simpl. rewrite IHhn. reflexivity. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile