proposition: Lemma Izero_nonNeg : forall (IS : IntegrationSpace), nonNegFunc (Izero IS).
proof: Proof. intros IS x xdf. unfold Izero. rewrite applyXscale, CRmult_0_l. apply CRle_refl. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions