proposition: Lemma IntegralZeroIsZero : forall {IS : IntegrationSpace}, Integral (@IntegrableZero IS) == 0.
proof: Proof. intros IS; unfold Integral. pose proof (IntegralCv (@IntegralRepresentationZero IS)). apply (series_cv_unique (fun _ : nat => I IS (Izero IS) (Izero_is_L IS))). assumption. apply (CR_cv_eq _ (fun _ => 0)). 2: apply CR_cv_const. intros. rewrite sum_const. unfold Izero. unfold Izero_is_L. rewrite Ihomogeneous. rewrite CRmult_0_l. rewrite CRmult_0_l. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase