proposition: Lemma SupDistanceToLinear_wd1 : forall x l1 r1 (H1:l1 < r1) l2 r2 (H2:l2 < r2), (l1 == l2 -> r1 == r2 -> QposEq (SupDistanceToLinear x H1) (SupDistanceToLinear x H2))%Q.
proof: Proof. induction x; intros l1 r1 H1 l2 r2 H2 Hl Hr. - unfold SupDistanceToLinear. unfold QposEq. simpl. rewrite -> Hl. rewrite -> Hr. reflexivity. - unfold QposEq. do 2 rewrite -> SupDistanceToLinear_glue. assert (X:(affineCombo (OpenUnitDual o) l1 r1==affineCombo (OpenUnitDual o) l2 r2)%Q). rewrite -> Hl. rewrite -> Hr. reflexivity. apply Qmax_compat. apply IHx1; auto. apply IHx2; auto. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.metric2.IntegrableFunction CoRN.model.metric2.BoundedFunction CoRN.model.metric2.CRmetric CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR CoRN.ftc.Integral CoRN.model.structures.StepQsec CoRN.model.structures.OpenUnit CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.QArith.Qabs CoRN.tactics.Qauto Coq.QArith.Qround CoRN.model.metric2.L1metric CoRN.model.metric2.LinfMetric CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields2 CoRN.model.metric2.Qmetric CoRN.reals.fast.ContinuousCorrect CoRN.ftc.IntegrationRules CoRN.ftc.MoreIntegrals CoRN.tactics.CornTac CoRN.model.metric2.LinfDistMonad