proposition: Lemma SupDistanceToLinear_glue : forall o l r a b (H:a < b), (proj1_sig (SupDistanceToLinear (glue o l r) H) == Qmax (proj1_sig (SupDistanceToLinear l (affineCombo_gt (OpenUnitDual o) H))) (proj1_sig (SupDistanceToLinear r (affineCombo_lt (OpenUnitDual o) H))))%Q.
proof: Proof. intros o l r a b H. unfold SupDistanceToLinear at 1. simpl. autorewrite with QposElim. reflexivity. 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