proposition: Lemma MeasureNonNeg : forall {IS : IntegrationSpace} (A : X (ElemFunc IS) -> Prop) (aInt : IntegrableSet A), 0 <= MeasureSet aInt.
proof: Proof. intros. apply (CRle_trans _ (Integral (@IntegrableZero IS))). rewrite IntegralZeroIsZero. apply CRle_refl. apply IntegralNonDecreasing. intros x xdf xdg. simpl. destruct xdg. apply CRlt_asym, CRzero_lt_one. apply CRle_refl. Qed.
imports: Logic.ConstructiveEpsilon QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTPositivity