proposition: Lemma StepFSupBall_nonneg : forall (e : Q) (a b : StepFS (msp_as_RSetoid X)), StepFSupBall e a b -> Qle (0#1) e.
proof: Proof. induction a. - induction b. intro H0. unfold StepFSupBall, StepFfoldProp in H0. simpl in H0. exact (msp_nonneg (msp X) e x x0 H0). intros [H0 _]. exact (IHb1 H0). - intros b H. unfold StepFSupBall, StepFfoldProp in H. simpl in H. unfold Ap in H. simpl in H. destruct (@Split X b o). destruct H. apply (IHa1 _ H). Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.metric2.StepFunctionSetoid CoRN.metric2.StepFunctionMonad CoRN.metric2.UniformContinuity CoRN.model.structures.OpenUnit Coq.QArith.QArith CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.metric2.Qmetric CoRN.metric2.Prelength CoRN.algebra.COrdFields2 CoRN.tactics.CornTac