proposition: Lemma L1Norm_nonneg : forall x, (0 <= (L1Norm x))%Q.
proof: Proof. intros x. apply Integral_resp_nonneg. unfold StepQ_le. rewriteStepF. set (g:=QleS 0). cut (StepFfoldProp ((compose g QabsS) ^@> x)). evalStepF. tauto. apply StepFfoldPropForall_Map. intros a. apply: Qabs_nonneg. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.structures.StepQsec CoRN.metric2.UniformContinuity CoRN.metric2.Prelength CoRN.model.structures.OpenUnit Coq.QArith.QArith CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.metric2.Qmetric CoRN.algebra.COrdFields2 CoRN.tactics.CornTac