proposition: Lemma Izero_is_zero : forall (IS : IntegrationSpace), I IS (Izero IS) (Izero_is_L IS) == 0.
proof: Proof. intros. unfold Izero. unfold Izero_is_L. rewrite Ihomogeneous. rewrite CRmult_0_l. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions