proposition: Lemma integralPositive : forall (IS : IntegrationSpace) (f : PartialFunction (X (ElemFunc IS))) (fL : L (ElemFunc IS) f), nonNegFunc f -> 0 <= I IS f fL.
proof: Proof. intros. apply (CRle_trans 0 (I IS (Izero IS) (Izero_is_L IS))). unfold Izero. unfold Izero_is_L. rewrite Ihomogeneous. rewrite CRmult_0_l. apply CRle_refl. apply INonDecreasing. intros. rewrite applyIzero. apply H. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions