proposition: Lemma SupDistanceToLinear_split : forall x o a b c (H0:a < c) (H1:c < b), (c == affineCombo (OpenUnitDual o) a b)%Q -> (Qmax (proj1_sig (SupDistanceToLinear (SplitL x o) H0)) (proj1_sig (SupDistanceToLinear (SplitR x o) H1)) == proj1_sig (SupDistanceToLinear x (Qlt_trans _ _ _ H0 H1)))%Q.
proof: Proof. induction x. intros o a b c H0 H1 Hc. unfold SupDistanceToLinear. simpl. autorewrite with QposElim. rewrite -> Hc. apply Qmax_affineCombo; auto with *. apply Qlt_trans with c; assumption. intros p a b c H0 H1 Hc. apply SplitLR_glue_ind; intros H. do 2 rewrite -> SupDistanceToLinear_glue. rewrite -> Qmax_assoc. rewrite -> IHx1. apply Qmax_compat; apply SupDistanceToLinear_wd1; try reflexivity; rewrite -> Hc; unfold affineCombo; simpl; field; auto with *. rewrite -> Hc. unfold affineCombo. simpl. field; auto with *. do 2 rewrite -> SupDistanceToLinear_glue. rewrite <- Qmax_assoc. rewrite -> IHx2. apply Qmax_compat; apply SupDistanceToLinear_wd1; try reflexivity; rewrite -> Hc; unfold affineCombo; simpl; field; auto with *. rewrite -> Hc. unfold affineCombo. simpl. field; auto with *. rewrite -> SupDistanceToLinear_glue. apply Qmax_compat; apply SupDistanceToLinear_wd1; try reflexivity; rewrite -> Hc; unfold affineCombo; simpl; rewrite -> H; field; auto with *. 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