proposition: Lemma StepQSup_plus : forall x y, (StepQSup (x + y) <= StepQSup x + StepQSup y )%Q.
proof: Proof. apply StepF_ind2; auto with *. intros s s0 t t0 Hs Ht. rewrite -> Hs, Ht; auto. intros o s s0 t t0 H0 H1. unfold StepQplus. rewriteStepF. repeat rewrite StepQSup_glue. eapply Qle_trans;[apply Qmax_le_compat;[apply H0|apply H1]|]. rewrite -> Qmax_plus_distr_l. apply Qmax_le_compat; apply: plus_resp_leEq_lft; simpl; auto with *. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.structures.StepQsec CoRN.metric2.Prelength CoRN.model.metric2.L1metric CoRN.model.metric2.LinfMetricMonad 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