proposition: Lemma Izero_is_L : forall (IS : IntegrationSpace), L (ElemFunc IS) (Izero IS).
proof: Proof. intros IS. unfold Izero. apply LscaleStable. apply IoneL. Defined.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions