proposition: Lemma SupDistanceToLinear_wd2 : forall x1 x2 a b (H: a < b), x1 == x2 -> QposEq (SupDistanceToLinear x1 H) (SupDistanceToLinear x2 H).
proof: Proof. induction x1. induction x2. intros a b H Hx. unfold SupDistanceToLinear. simpl in *. autorewrite with QposElim. change (x == x0)%Q in Hx. unfold QposEq. simpl. rewrite -> Hx. reflexivity. intros a b H Hx. destruct Hx as [H0 H1] using (eq_glue_ind x2_1). unfold QposEq. simpl. rewrite -> SupDistanceToLinear_glue. unfold QposEq in IHx2_1. rewrite <- IHx2_1; auto with *. unfold QposEq in IHx2_2. rewrite <- IHx2_2; auto with *. unfold SupDistanceToLinear. simpl. autorewrite with QposElim. rewrite <- Qmax_assoc. rewrite -> (Qmax_assoc (affineCombo (OpenUnitDual o) a b - x)). rewrite -> (Qmax_comm (affineCombo (OpenUnitDual o) a b - x)). rewrite <- (Qmax_assoc (x - affineCombo (OpenUnitDual o) a b)). rewrite -> Qmax_assoc. symmetry. apply Qmax_compat. rewrite <- Qle_max_l. apply: plus_resp_leEq_lft;simpl;auto with *. rewrite <- Qle_max_r. apply: plus_resp_leEq;simpl; auto with *. intros x2 a b H Hx. destruct Hx as [H0 H1] using (glue_eq_ind x1_1). unfold QposEq. rewrite -> SupDistanceToLinear_glue. unfold QposEq in IHx1_1. rewrite -> (IHx1_1 _ _ _ (affineCombo_gt (OpenUnitDual o) H) H0). unfold QposEq in IHx1_2. rewrite -> (IHx1_2 _ _ _ (affineCombo_lt (OpenUnitDual o) H) H1). rewrite -> SupDistanceToLinear_split; [|reflexivity]. apply SupDistanceToLinear_wd1; try 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