proposition: Lemma Integral_plus:forall s t, ((IntegralQ s)+(IntegralQ t)==(IntegralQ (s + t)))%Q.
proof: Proof. apply StepF_ind2; try reflexivity. intros s s0 t t0 Hs Ht. rewrite -> Hs, Ht; auto. intros o s s0 t t0 H0 H1. unfold StepQplus. rewriteStepF. replace LHS with (o*(IntegralQ s + IntegralQ t) + (1-o)*(IntegralQ s0 + IntegralQ t0))%Q by simpl; ring. rewrite -> H0, H1. reflexivity. 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